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  3124  disjiun  4084  f1imass  5920  riota5f  6003  tfrexlem  6505  tfrcl  6535  nnsucuniel  6668  nntr2  6676  pw2f1odclem  7025  fopwdom  7027  fidceq  7061  fisbth  7077  fidcen  7093  fientri3  7112  unsnfidcex  7117  undifdc  7121  iunfidisj  7150  fiuni  7182  ordiso2  7239  nninfninc  7327  acfun  7427  2omotaplemap  7481  ccfunen  7488  addcmpblnq  7592  mulcmpblnq  7593  ordpipqqs  7599  addcmpblnq0  7668  mulcmpblnq0  7669  prml  7702  addlocpr  7761  prmuloc  7791  mullocpr  7796  ltexprlemopl  7826  ltexprlemopu  7828  ltexprlemloc  7832  ltexprlemrl  7835  ltexprlemru  7837  addcanprleml  7839  addcanprlemu  7840  aptiprleml  7864  ltmprr  7867  cauappcvgprlemopl  7871  cauappcvgprlemopu  7873  cauappcvgprlemloc  7877  caucvgprlemopl  7894  caucvgprlemopu  7896  caucvgprlemloc  7900  caucvgprprlemopu  7924  caucvgprprlemloc  7928  caucvgprprlemexbt  7931  caucvgprprlemaddq  7933  suplocexprlemrl  7942  suplocexprlemdisj  7945  suplocexprlemloc  7946  suplocexprlemub  7948  addcmpblnr  7964  mulcmpblnrlemg  7965  mulcmpblnr  7966  ltsrprg  7972  mulgt0sr  8003  caucvgsrlemgt1  8020  suplocsrlemb  8031  axmulcl  8091  axcaucvglemres  8124  axpre-suploclemres  8126  axpre-suploc  8127  cnegexlem1  8359  negeu  8375  add20  8659  apreap  8772  cru  8787  apsym  8791  apcotr  8792  apadd1  8793  apneg  8796  mulext1  8797  mulge0  8804  mulap0  8839  divdivdivap  8898  prodgt0  9037  ltmul12a  9045  lt2mul2div  9064  ledivdiv  9075  lediv12a  9079  qapne  9878  xleadd1a  10113  ixxss12  10146  elfz0ubfz0  10365  qtri3or  10506  exbtwnzlemstep  10513  exbtwnzlemex  10515  exbtwnz  10516  rebtwn2zlemstep  10518  rebtwn2z  10520  btwnzge0  10566  iseqf1olemqf1o  10774  mulexpzap  10847  leexp1a  10862  hashen  11052  fihashdom  11072  hashun  11074  swrdccatin1  11315  pfxccatin12lem3  11322  pfxccat3  11324  cjap  11489  cvg1nlemres  11568  rsqrmo  11610  abslt  11671  abs3lem  11694  cau3lem  11697  rexanre  11803  xrmaxltsup  11841  climcau  11930  sumeq2  11942  summodc  11967  fisumss  11976  fsum2d  12019  fsumabs  12049  fsumiun  12061  prodeq2  12141  prodmodclem2  12161  fprodcl2lem  12189  fprodap0  12205  fprod2d  12207  fprodrec  12213  fprodap0f  12220  fprodle  12224  eirrap  12362  divalglemeunn  12505  divalglemeuneg  12507  bezoutlemnewy  12590  bezoutlemstep  12591  bezoutlemmain  12592  bezoutlembi  12599  bezoutlemeu  12601  qredeu  12692  isprm5lem  12736  pw2dvdseu  12763  sqrt2irrap  12775  pythagtriplem2  12862  pythagtrip  12879  pclemub  12883  pcqmul  12899  pcexp  12905  pcneg  12921  pcprmpw2  12929  pcadd  12936  prmpwdvds  12951  4sqlem13m  12999  ennnfonelemg  13047  ennnfonelemrnh  13060  ctiunctlemfo  13083  nninfdclemf1  13096  imasival  13412  sgrppropd  13519  ismndd  13543  mndpropd  13546  mhmeql  13598  mhmmnd  13726  mulgfng  13734  issubg4m  13803  ssnmz  13821  conjnmzb  13890  rngpropd  13992  ringpropd  14075  dvdsrtr  14139  islmod  14329  mplsubgfilemcl  14742  restbasg  14921  cnpnei  14972  cnptoprest2  14993  cnpdis  14995  lmtopcnp  15003  txcnp  15024  ismet2  15107  blininf  15177  metss2lem  15250  xmettxlem  15262  xmettx  15263  metcnp  15265  metcnpi3  15270  addcncntoplem  15314  fsumcncntop  15320  mulc1cncf  15342  cncfco  15344  mulcncf  15361  dedekindeulemuub  15370  dedekindeu  15376  dedekindicclemuub  15379  ivthinclemloc  15394  ivthinc  15396  limcimo  15418  limccnp2cntop  15430  dveflem  15479  plyf  15490  plyco  15512  plycj  15514  dvply2g  15519  logbgcd1irrap  15723  perfectlem2  15753  lgsdilem  15785  lgsquad2lem2  15840  lgsquad3  15842  2sqlem5  15877  2sqlem9  15882  usgredg4  16095  usgr1eop  16125  usgr1vr  16128  subuhgr  16152  subumgr  16154  subusgr  16155  clwwlknonex2lem2  16318  2omap  16654  pw1map  16656  qdencn  16694  apdiff  16719  qdiff  16720  gfsumval  16748