Theorem simprl 414

Description: Simplification of a conjunction.

Assertion

Ref	Expression
simprl	⊢ ((φ ⋀ (ψ ⋀ χ)) → ψ)

Proof of Theorem simprl

Step	Hyp	Ref	Expression
1		id 59	. 2 ⊢ (ψ → ψ)
2	1	ad2antrl 406	1 ⊢ ((φ ⋀ (ψ ⋀ χ)) → ψ)

Syntax hints:   → wi 3   ⋀ wa 221

This theorem is referenced by:  xp0r 3325  imainss 3548  unielxp 4167  1stconst 4190  2ndconst 4191  ac6sfilem3 4590  rankxplim3 4860  cnegexlem1 5499  muladd 5575  xrre 5723  divass 5887  divadddiv 5923  divdivdiv 5924  conjmul 5937  ltmul12a 5985  lemulge11 5992  ledivp1 6050  modmul1 6478  elfzle1 6611  2shfti 6717  expordi 6797  le2sq2 6829  expnbnd 6852  fsumcom 7231  fsummulc1 7236  fsumdivc 7238  serzcmp0 7258  climaddc1 7321  climaddc2 7322  climsubc2 7334  climcmpc1 7342  cvgratlem5 7459  acdc3lem 7697  acdclem 7706  cnco 7978  blelrn 8058  blss 8063  metequiv 8091  metcnplem 8097  metcnpi3 8103  metcnpi4 8104  lmbr 8139  lmnn 8146  lmsslem 8163  metelcls 8176  metcnp4 8181  xplmi 8184  lmcau 8207  bcthlem21 8230  grpidinvlem1 8261  grpidinvlem2 8262  grpinvid1 8289  grpinvid2 8290  grplcan 8292  abl4 8346  nvmf 8513  nvsubadd 8522  nvnpcan 8527  nvabs 8548  nvlmle 8580  lnomul 8675  blocnilem 8719  blocni 8720  ubthlem3 8789  ubthlem7 8793  ubthlem8 8794  ubthlem10 8796  minveclem30 8834  htthlem10 8891  psdmrn 8910  psref 8911  spansncol 9767  unoplin 10124  hmoplin 10146  hmops 10224  hmopm 10225  hmopco 10227  lnopconi 10242  lnfnconi 10269  adjmul 10304  adjadd 10305  mdslmd1lem1 10533  atn0 10553  irredi 10603  mdsymlem3 10614  ghomf1olem 10681  cljo 10834  clme 10835  jidd 10840  midd 10841  definc 10869  domncnt 10872  ranncnt 10873  toplat 10884  trnij 11160  imonclem 11268  idmon 11272  domsubc 11306  xpss2 11404  finsschain 11425  ordiso 11426  ordtypelem6 11432  ordtypelem7 11433  hartog 11436  cnpnei 11472  elsubsp 11477  subntr 11482  cnsubsp 11483  cptclsscpt 11489  alexsublem3 11498  alexsublem4 11499  dfcon2 11501  subtopmetlem 11505  subtopmet 11506  reconnlem2 11508  reconnlem4 11510  reconnlem5 11511  2ndcsb 11537  2ndcctbss 11539  isfne3 11543  fnetr 11556  reftr 11558  fnessref 11564  refssfne 11565  locfincf 11577  comppfsc 11578  neibastop1 11579  neibastop2lem2 11581  neibastop3 11585  topjoin 11588  fnemeet1 11589  fnemeet2 11590  fbssint 11626  fbunfip 11631  isufil2 11650  filssufil 11656  filufint 11659  fixufil 11661  ufinffr 11663  ufilen 11664  limfilcf 11683  cnpfillim 11686  elfilmap3 11692  rnelfmlem 11698  rnelfm 11699  fmfnfmlem2 11701  fmfnfmlem4 11703  fmufil 11705  isfclus 11718  fcluscf 11724  fclsfnflim 11726  flimfnfcls 11727  fcluscnp 11730  fcluscomplem 11732  tosdir 11755  filnetlem3 11765  filnetlem4 11766  filnetlem5 11767  ssga 11777  sdc 11877  subspopn 11900  subspcld 11901  metsstop 11909  blhalf 11911  cnres2 11951  lmtlm 11969  2txcn 11982  txsubsp 11983  ismtyhmeolem 12006  ismtybndlem 12008  heiborlem18 12028  heiborlem36 12046  rrncms 12075  rrntotbndlem2 12077  phtpyco 12098

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 145  df-an 223

Copyright terms: Public domain