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  3092  disjiun  4042  f1imass  5850  riota5f  5931  tfrexlem  6427  tfrcl  6457  nnsucuniel  6588  nntr2  6596  pw2f1odclem  6938  fopwdom  6940  fidceq  6973  fisbth  6987  fientri3  7019  unsnfidcex  7024  undifdc  7028  iunfidisj  7055  fiuni  7087  ordiso2  7144  nninfninc  7232  acfun  7326  2omotaplemap  7376  ccfunen  7383  addcmpblnq  7487  mulcmpblnq  7488  ordpipqqs  7494  addcmpblnq0  7563  mulcmpblnq0  7564  prml  7597  addlocpr  7656  prmuloc  7686  mullocpr  7691  ltexprlemopl  7721  ltexprlemopu  7723  ltexprlemloc  7727  ltexprlemrl  7730  ltexprlemru  7732  addcanprleml  7734  addcanprlemu  7735  aptiprleml  7759  ltmprr  7762  cauappcvgprlemopl  7766  cauappcvgprlemopu  7768  cauappcvgprlemloc  7772  caucvgprlemopl  7789  caucvgprlemopu  7791  caucvgprlemloc  7795  caucvgprprlemopu  7819  caucvgprprlemloc  7823  caucvgprprlemexbt  7826  caucvgprprlemaddq  7828  suplocexprlemrl  7837  suplocexprlemdisj  7840  suplocexprlemloc  7841  suplocexprlemub  7843  addcmpblnr  7859  mulcmpblnrlemg  7860  mulcmpblnr  7861  ltsrprg  7867  mulgt0sr  7898  caucvgsrlemgt1  7915  suplocsrlemb  7926  axmulcl  7986  axcaucvglemres  8019  axpre-suploclemres  8021  axpre-suploc  8022  cnegexlem1  8254  negeu  8270  add20  8554  apreap  8667  cru  8682  apsym  8686  apcotr  8687  apadd1  8688  apneg  8691  mulext1  8692  mulge0  8699  mulap0  8734  divdivdivap  8793  prodgt0  8932  ltmul12a  8940  lt2mul2div  8959  ledivdiv  8970  lediv12a  8974  qapne  9767  xleadd1a  10002  ixxss12  10035  elfz0ubfz0  10254  qtri3or  10390  exbtwnzlemstep  10397  exbtwnzlemex  10399  exbtwnz  10400  rebtwn2zlemstep  10402  rebtwn2z  10404  btwnzge0  10450  iseqf1olemqf1o  10658  mulexpzap  10731  leexp1a  10746  hashen  10936  fihashdom  10955  hashun  10957  cjap  11261  cvg1nlemres  11340  rsqrmo  11382  abslt  11443  abs3lem  11466  cau3lem  11469  rexanre  11575  xrmaxltsup  11613  climcau  11702  sumeq2  11714  summodc  11738  fisumss  11747  fsum2d  11790  fsumabs  11820  fsumiun  11832  prodeq2  11912  prodmodclem2  11932  fprodcl2lem  11960  fprodap0  11976  fprod2d  11978  fprodrec  11984  fprodap0f  11991  fprodle  11995  eirrap  12133  divalglemeunn  12276  divalglemeuneg  12278  bezoutlemnewy  12361  bezoutlemstep  12362  bezoutlemmain  12363  bezoutlembi  12370  bezoutlemeu  12372  qredeu  12463  isprm5lem  12507  pw2dvdseu  12534  sqrt2irrap  12546  pythagtriplem2  12633  pythagtrip  12650  pclemub  12654  pcqmul  12670  pcexp  12676  pcneg  12692  pcprmpw2  12700  pcadd  12707  prmpwdvds  12722  4sqlem13m  12770  ennnfonelemg  12818  ennnfonelemrnh  12831  ctiunctlemfo  12854  nninfdclemf1  12867  imasival  13182  sgrppropd  13289  ismndd  13313  mndpropd  13316  mhmeql  13368  mhmmnd  13496  mulgfng  13504  issubg4m  13573  ssnmz  13591  conjnmzb  13660  rngpropd  13761  ringpropd  13844  dvdsrtr  13907  islmod  14097  mplsubgfilemcl  14505  restbasg  14684  cnpnei  14735  cnptoprest2  14756  cnpdis  14758  lmtopcnp  14766  txcnp  14787  ismet2  14870  blininf  14940  metss2lem  15013  xmettxlem  15025  xmettx  15026  metcnp  15028  metcnpi3  15033  addcncntoplem  15077  fsumcncntop  15083  mulc1cncf  15105  cncfco  15107  mulcncf  15124  dedekindeulemuub  15133  dedekindeu  15139  dedekindicclemuub  15142  ivthinclemloc  15157  ivthinc  15159  limcimo  15181  limccnp2cntop  15193  dveflem  15242  plyf  15253  plyco  15275  plycj  15277  dvply2g  15282  logbgcd1irrap  15486  perfectlem2  15516  lgsdilem  15548  lgsquad2lem2  15603  lgsquad3  15605  2sqlem5  15640  2sqlem9  15645  2omap  16006  qdencn  16040  apdiff  16061