Theorem simplrl 535

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  3078  disjiun  4024  f1imass  5817  riota5f  5898  tfrexlem  6387  tfrcl  6417  nnsucuniel  6548  nntr2  6556  pw2f1odclem  6890  fopwdom  6892  fidceq  6925  fisbth  6939  fientri3  6971  unsnfidcex  6976  undifdc  6980  iunfidisj  7005  fiuni  7037  ordiso2  7094  nninfninc  7182  acfun  7267  2omotaplemap  7317  ccfunen  7324  addcmpblnq  7427  mulcmpblnq  7428  ordpipqqs  7434  addcmpblnq0  7503  mulcmpblnq0  7504  prml  7537  addlocpr  7596  prmuloc  7626  mullocpr  7631  ltexprlemopl  7661  ltexprlemopu  7663  ltexprlemloc  7667  ltexprlemrl  7670  ltexprlemru  7672  addcanprleml  7674  addcanprlemu  7675  aptiprleml  7699  ltmprr  7702  cauappcvgprlemopl  7706  cauappcvgprlemopu  7708  cauappcvgprlemloc  7712  caucvgprlemopl  7729  caucvgprlemopu  7731  caucvgprlemloc  7735  caucvgprprlemopu  7759  caucvgprprlemloc  7763  caucvgprprlemexbt  7766  caucvgprprlemaddq  7768  suplocexprlemrl  7777  suplocexprlemdisj  7780  suplocexprlemloc  7781  suplocexprlemub  7783  addcmpblnr  7799  mulcmpblnrlemg  7800  mulcmpblnr  7801  ltsrprg  7807  mulgt0sr  7838  caucvgsrlemgt1  7855  suplocsrlemb  7866  axmulcl  7926  axcaucvglemres  7959  axpre-suploclemres  7961  axpre-suploc  7962  cnegexlem1  8194  negeu  8210  add20  8493  apreap  8606  cru  8621  apsym  8625  apcotr  8626  apadd1  8627  apneg  8630  mulext1  8631  mulge0  8638  mulap0  8673  divdivdivap  8732  prodgt0  8871  ltmul12a  8879  lt2mul2div  8898  ledivdiv  8909  lediv12a  8913  qapne  9704  xleadd1a  9939  ixxss12  9972  elfz0ubfz0  10191  qtri3or  10310  exbtwnzlemstep  10316  exbtwnzlemex  10318  exbtwnz  10319  rebtwn2zlemstep  10321  rebtwn2z  10323  btwnzge0  10369  iseqf1olemqf1o  10577  mulexpzap  10650  leexp1a  10665  hashen  10855  fihashdom  10874  hashun  10876  cjap  11050  cvg1nlemres  11129  rsqrmo  11171  abslt  11232  abs3lem  11255  cau3lem  11258  rexanre  11364  xrmaxltsup  11401  climcau  11490  sumeq2  11502  summodc  11526  fisumss  11535  fsum2d  11578  fsumabs  11608  fsumiun  11620  prodeq2  11700  prodmodclem2  11720  fprodcl2lem  11748  fprodap0  11764  fprod2d  11766  fprodrec  11772  fprodap0f  11779  fprodle  11783  eirrap  11921  divalglemeunn  12062  divalglemeuneg  12064  bezoutlemnewy  12133  bezoutlemstep  12134  bezoutlemmain  12135  bezoutlembi  12142  bezoutlemeu  12144  qredeu  12235  isprm5lem  12279  pw2dvdseu  12306  sqrt2irrap  12318  pythagtriplem2  12404  pythagtrip  12421  pclemub  12425  pcqmul  12441  pcexp  12447  pcneg  12463  pcprmpw2  12471  pcadd  12478  prmpwdvds  12493  4sqlem13m  12541  ennnfonelemg  12560  ennnfonelemrnh  12573  ctiunctlemfo  12596  nninfdclemf1  12609  imasival  12889  sgrppropd  12996  ismndd  13018  mndpropd  13021  mhmeql  13064  mhmmnd  13186  mulgfng  13194  issubg4m  13263  ssnmz  13281  conjnmzb  13350  rngpropd  13451  ringpropd  13534  dvdsrtr  13597  islmod  13787  restbasg  14336  cnpnei  14387  cnptoprest2  14408  cnpdis  14410  lmtopcnp  14418  txcnp  14439  ismet2  14522  blininf  14592  metss2lem  14665  xmettxlem  14677  xmettx  14678  metcnp  14680  metcnpi3  14685  addcncntoplem  14719  fsumcncntop  14724  mulc1cncf  14744  cncfco  14746  mulcncf  14762  dedekindeulemuub  14771  dedekindeu  14777  dedekindicclemuub  14780  ivthinclemloc  14795  ivthinc  14797  limcimo  14819  limccnp2cntop  14831  dveflem  14872  plyf  14883  logbgcd1irrap  15102  lgsdilem  15143  2sqlem5  15206  2sqlem9  15211  qdencn  15517  apdiff  15538