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  3082  disjiun  4029  f1imass  5824  riota5f  5905  tfrexlem  6401  tfrcl  6431  nnsucuniel  6562  nntr2  6570  pw2f1odclem  6904  fopwdom  6906  fidceq  6939  fisbth  6953  fientri3  6985  unsnfidcex  6990  undifdc  6994  iunfidisj  7021  fiuni  7053  ordiso2  7110  nninfninc  7198  acfun  7290  2omotaplemap  7340  ccfunen  7347  addcmpblnq  7451  mulcmpblnq  7452  ordpipqqs  7458  addcmpblnq0  7527  mulcmpblnq0  7528  prml  7561  addlocpr  7620  prmuloc  7650  mullocpr  7655  ltexprlemopl  7685  ltexprlemopu  7687  ltexprlemloc  7691  ltexprlemrl  7694  ltexprlemru  7696  addcanprleml  7698  addcanprlemu  7699  aptiprleml  7723  ltmprr  7726  cauappcvgprlemopl  7730  cauappcvgprlemopu  7732  cauappcvgprlemloc  7736  caucvgprlemopl  7753  caucvgprlemopu  7755  caucvgprlemloc  7759  caucvgprprlemopu  7783  caucvgprprlemloc  7787  caucvgprprlemexbt  7790  caucvgprprlemaddq  7792  suplocexprlemrl  7801  suplocexprlemdisj  7804  suplocexprlemloc  7805  suplocexprlemub  7807  addcmpblnr  7823  mulcmpblnrlemg  7824  mulcmpblnr  7825  ltsrprg  7831  mulgt0sr  7862  caucvgsrlemgt1  7879  suplocsrlemb  7890  axmulcl  7950  axcaucvglemres  7983  axpre-suploclemres  7985  axpre-suploc  7986  cnegexlem1  8218  negeu  8234  add20  8518  apreap  8631  cru  8646  apsym  8650  apcotr  8651  apadd1  8652  apneg  8655  mulext1  8656  mulge0  8663  mulap0  8698  divdivdivap  8757  prodgt0  8896  ltmul12a  8904  lt2mul2div  8923  ledivdiv  8934  lediv12a  8938  qapne  9730  xleadd1a  9965  ixxss12  9998  elfz0ubfz0  10217  qtri3or  10347  exbtwnzlemstep  10354  exbtwnzlemex  10356  exbtwnz  10357  rebtwn2zlemstep  10359  rebtwn2z  10361  btwnzge0  10407  iseqf1olemqf1o  10615  mulexpzap  10688  leexp1a  10703  hashen  10893  fihashdom  10912  hashun  10914  cjap  11088  cvg1nlemres  11167  rsqrmo  11209  abslt  11270  abs3lem  11293  cau3lem  11296  rexanre  11402  xrmaxltsup  11440  climcau  11529  sumeq2  11541  summodc  11565  fisumss  11574  fsum2d  11617  fsumabs  11647  fsumiun  11659  prodeq2  11739  prodmodclem2  11759  fprodcl2lem  11787  fprodap0  11803  fprod2d  11805  fprodrec  11811  fprodap0f  11818  fprodle  11822  eirrap  11960  divalglemeunn  12103  divalglemeuneg  12105  bezoutlemnewy  12188  bezoutlemstep  12189  bezoutlemmain  12190  bezoutlembi  12197  bezoutlemeu  12199  qredeu  12290  isprm5lem  12334  pw2dvdseu  12361  sqrt2irrap  12373  pythagtriplem2  12460  pythagtrip  12477  pclemub  12481  pcqmul  12497  pcexp  12503  pcneg  12519  pcprmpw2  12527  pcadd  12534  prmpwdvds  12549  4sqlem13m  12597  ennnfonelemg  12645  ennnfonelemrnh  12658  ctiunctlemfo  12681  nninfdclemf1  12694  imasival  13008  sgrppropd  13115  ismndd  13139  mndpropd  13142  mhmeql  13194  mhmmnd  13322  mulgfng  13330  issubg4m  13399  ssnmz  13417  conjnmzb  13486  rngpropd  13587  ringpropd  13670  dvdsrtr  13733  islmod  13923  restbasg  14488  cnpnei  14539  cnptoprest2  14560  cnpdis  14562  lmtopcnp  14570  txcnp  14591  ismet2  14674  blininf  14744  metss2lem  14817  xmettxlem  14829  xmettx  14830  metcnp  14832  metcnpi3  14837  addcncntoplem  14881  fsumcncntop  14887  mulc1cncf  14909  cncfco  14911  mulcncf  14928  dedekindeulemuub  14937  dedekindeu  14943  dedekindicclemuub  14946  ivthinclemloc  14961  ivthinc  14963  limcimo  14985  limccnp2cntop  14997  dveflem  15046  plyf  15057  plyco  15079  plycj  15081  dvply2g  15086  logbgcd1irrap  15290  perfectlem2  15320  lgsdilem  15352  lgsquad2lem2  15407  lgsquad3  15409  2sqlem5  15444  2sqlem9  15449  2omap  15726  qdencn  15758  apdiff  15779