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  3139  disjiun  4109  f1imass  5953  riota5f  6038  tfrexlem  6578  tfrcl  6608  nnsucuniel  6741  nntr2  6749  pw2f1odclem  7100  fopwdom  7102  fidceq  7137  fisbth  7153  fidcen  7169  fientri3  7188  unsnfidcex  7193  undifdc  7197  iunfidisj  7226  fiuni  7278  2omap  7282  ordiso2  7339  nninfninc  7427  acfun  7527  2omotaplemap  7587  ccfunen  7594  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  addcmpblnq0  7774  mulcmpblnq0  7775  prml  7808  addlocpr  7867  prmuloc  7897  mullocpr  7902  ltexprlemopl  7932  ltexprlemopu  7934  ltexprlemloc  7938  ltexprlemrl  7941  ltexprlemru  7943  addcanprleml  7945  addcanprlemu  7946  aptiprleml  7970  ltmprr  7973  cauappcvgprlemopl  7977  cauappcvgprlemopu  7979  cauappcvgprlemloc  7983  caucvgprlemopl  8000  caucvgprlemopu  8002  caucvgprlemloc  8006  caucvgprprlemopu  8030  caucvgprprlemloc  8034  caucvgprprlemexbt  8037  caucvgprprlemaddq  8039  suplocexprlemrl  8048  suplocexprlemdisj  8051  suplocexprlemloc  8052  suplocexprlemub  8054  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  ltsrprg  8078  mulgt0sr  8109  caucvgsrlemgt1  8126  suplocsrlemb  8137  axmulcl  8197  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  cnegexlem1  8465  negeu  8481  add20  8766  apreap  8879  cru  8894  apsym  8898  apcotr  8899  apadd1  8900  apneg  8903  mulext1  8904  mulge0  8911  mulap0  8946  divdivdivap  9007  prodgt0  9146  ltmul12a  9154  lt2mul2div  9173  ledivdiv  9184  lediv12a  9188  qapne  9992  xleadd1a  10228  ixxss12  10261  elfz0ubfz0  10484  qtri3or  10627  exbtwnzlemstep  10634  exbtwnzlemex  10636  exbtwnz  10637  rebtwn2zlemstep  10639  rebtwn2z  10641  btwnzge0  10687  iseqf1olemqf1o  10895  mulexpzap  10968  leexp1a  10983  hashen  11175  fihashdom  11195  hashun  11197  swrdccatin1  11445  pfxccatin12lem3  11452  pfxccat3  11454  cjap  11619  cvg1nlemres  11698  rsqrmo  11740  abslt  11801  abs3lem  11824  cau3lem  11827  rexanre  11933  xrmaxltsup  11971  climcau  12060  sumeq2  12072  summodc  12097  fisumss  12106  fsum2d  12149  fsumabs  12179  fsumiun  12191  prodeq2  12271  prodmodclem2  12291  fprodcl2lem  12319  fprodap0  12335  fprod2d  12337  fprodrec  12343  fprodap0f  12350  fprodle  12354  eirrap  12492  divalglemeunn  12635  divalglemeuneg  12637  bezoutlemnewy  12720  bezoutlemstep  12721  bezoutlemmain  12722  bezoutlembi  12729  bezoutlemeu  12731  qredeu  12822  isprm5lem  12866  pw2dvdseu  12893  sqrt2irrap  12905  pythagtriplem2  12992  pythagtrip  13009  pclemub  13013  pcqmul  13029  pcexp  13035  pcneg  13051  pcprmpw2  13059  pcadd  13066  prmpwdvds  13081  4sqlem13m  13129  ballotfilemsf1o  13204  ennnfonelemg  13241  ennnfonelemrnh  13254  ctiunctlemfo  13277  nninfdclemf1  13290  imasival  13573  sgrppropd  13679  ismndd  13701  mndpropd  13704  mhmeql  13750  mhmmnd  13872  mulgfng  13880  issubg4m  13949  ssnmz  13967  conjnmzb  14036  gfsumval  14105  rngpropd  14197  ringpropd  14284  dvdsrtr  14349  aprlring  14541  islmod  14568  mplsubgfilemcl  14983  restbasg  15162  cnpnei  15213  cnptoprest2  15234  cnpdis  15236  lmtopcnp  15244  txcnp  15265  ismet2  15348  blininf  15418  metss2lem  15491  xmettxlem  15503  xmettx  15504  metcnp  15506  metcnpi3  15511  addcncntoplem  15555  fsumcncntop  15561  mulc1cncf  15583  cncfco  15585  mulcncf  15602  dedekindeulemuub  15611  dedekindeu  15617  dedekindicclemuub  15620  ivthinclemloc  15635  ivthinc  15637  limcimo  15659  limccnp2cntop  15671  dveflem  15720  plyf  15731  plyco  15753  plycj  15755  dvply2g  15760  logbgcd1irrap  15964  perfectlem2  15997  lgsdilem  16029  lgsquad2lem2  16084  lgsquad3  16086  2sqlem5  16121  2sqlem9  16126  usgredg4  16339  usgr1eop  16369  usgr1vr  16372  subuhgr  16396  subumgr  16398  subusgr  16399  clwwlknonex2lem2  16562  pw1map  16908  qdencn  16946  apdiff  16971  qdiff  16972