Theorem simplrl 537

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simplrl	⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Proof of Theorem simplrl

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 489	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  rmob  3135  disjiun  4103  f1imass  5946  riota5f  6029  tfrexlem  6564  tfrcl  6594  nnsucuniel  6727  nntr2  6735  pw2f1odclem  7086  fopwdom  7088  fidceq  7123  fisbth  7139  fidcen  7155  fientri3  7174  unsnfidcex  7179  undifdc  7183  iunfidisj  7212  fiuni  7264  2omap  7268  ordiso2  7325  nninfninc  7413  acfun  7513  2omotaplemap  7567  ccfunen  7574  addcmpblnq  7678  mulcmpblnq  7679  ordpipqqs  7685  addcmpblnq0  7754  mulcmpblnq0  7755  prml  7788  addlocpr  7847  prmuloc  7877  mullocpr  7882  ltexprlemopl  7912  ltexprlemopu  7914  ltexprlemloc  7918  ltexprlemrl  7921  ltexprlemru  7923  addcanprleml  7925  addcanprlemu  7926  aptiprleml  7950  ltmprr  7953  cauappcvgprlemopl  7957  cauappcvgprlemopu  7959  cauappcvgprlemloc  7963  caucvgprlemopl  7980  caucvgprlemopu  7982  caucvgprlemloc  7986  caucvgprprlemopu  8010  caucvgprprlemloc  8014  caucvgprprlemexbt  8017  caucvgprprlemaddq  8019  suplocexprlemrl  8028  suplocexprlemdisj  8031  suplocexprlemloc  8032  suplocexprlemub  8034  addcmpblnr  8050  mulcmpblnrlemg  8051  mulcmpblnr  8052  ltsrprg  8058  mulgt0sr  8089  caucvgsrlemgt1  8106  suplocsrlemb  8117  axmulcl  8177  axcaucvglemres  8210  axpre-suploclemres  8212  axpre-suploc  8213  cnegexlem1  8444  negeu  8460  add20  8744  apreap  8857  cru  8872  apsym  8876  apcotr  8877  apadd1  8878  apneg  8881  mulext1  8882  mulge0  8889  mulap0  8924  divdivdivap  8983  prodgt0  9122  ltmul12a  9130  lt2mul2div  9149  ledivdiv  9160  lediv12a  9164  qapne  9967  xleadd1a  10202  ixxss12  10235  elfz0ubfz0  10455  qtri3or  10596  exbtwnzlemstep  10603  exbtwnzlemex  10605  exbtwnz  10606  rebtwn2zlemstep  10608  rebtwn2z  10610  btwnzge0  10656  iseqf1olemqf1o  10864  mulexpzap  10937  leexp1a  10952  hashen  11142  fihashdom  11162  hashun  11164  swrdccatin1  11410  pfxccatin12lem3  11417  pfxccat3  11419  cjap  11584  cvg1nlemres  11663  rsqrmo  11705  abslt  11766  abs3lem  11789  cau3lem  11792  rexanre  11898  xrmaxltsup  11936  climcau  12025  sumeq2  12037  summodc  12062  fisumss  12071  fsum2d  12114  fsumabs  12144  fsumiun  12156  prodeq2  12236  prodmodclem2  12256  fprodcl2lem  12284  fprodap0  12300  fprod2d  12302  fprodrec  12308  fprodap0f  12315  fprodle  12319  eirrap  12457  divalglemeunn  12600  divalglemeuneg  12602  bezoutlemnewy  12685  bezoutlemstep  12686  bezoutlemmain  12687  bezoutlembi  12694  bezoutlemeu  12696  qredeu  12787  isprm5lem  12831  pw2dvdseu  12858  sqrt2irrap  12870  pythagtriplem2  12957  pythagtrip  12974  pclemub  12978  pcqmul  12994  pcexp  13000  pcneg  13016  pcprmpw2  13024  pcadd  13031  prmpwdvds  13046  4sqlem13m  13094  ennnfonelemg  13143  ennnfonelemrnh  13156  ctiunctlemfo  13179  nninfdclemf1  13192  imasival  13508  sgrppropd  13615  ismndd  13639  mndpropd  13642  mhmeql  13694  mhmmnd  13822  mulgfng  13830  issubg4m  13899  ssnmz  13917  conjnmzb  13986  rngpropd  14088  ringpropd  14171  dvdsrtr  14235  islmod  14426  mplsubgfilemcl  14841  restbasg  15020  cnpnei  15071  cnptoprest2  15092  cnpdis  15094  lmtopcnp  15102  txcnp  15123  ismet2  15206  blininf  15276  metss2lem  15349  xmettxlem  15361  xmettx  15362  metcnp  15364  metcnpi3  15369  addcncntoplem  15413  fsumcncntop  15419  mulc1cncf  15441  cncfco  15443  mulcncf  15460  dedekindeulemuub  15469  dedekindeu  15475  dedekindicclemuub  15478  ivthinclemloc  15493  ivthinc  15495  limcimo  15517  limccnp2cntop  15529  dveflem  15578  plyf  15589  plyco  15611  plycj  15613  dvply2g  15618  logbgcd1irrap  15822  perfectlem2  15855  lgsdilem  15887  lgsquad2lem2  15942  lgsquad3  15944  2sqlem5  15979  2sqlem9  15984  usgredg4  16197  usgr1eop  16227  usgr1vr  16230  subuhgr  16254  subumgr  16256  subusgr  16257  clwwlknonex2lem2  16420  pw1map  16756  qdencn  16794  apdiff  16819  qdiff  16820  gfsumval  16848