Theorem simplrl 524

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 108	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜓)
2	1	ad2antlr 480	1 ⊢ (((𝜑 ∧ (𝜓 ∧ 𝜒)) ∧ 𝜃) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  rmob  3001  disjiun  3924  f1imass  5675  riota5f  5754  tfrexlem  6231  tfrcl  6261  nnsucuniel  6391  nntr2  6399  fopwdom  6730  fidceq  6763  fisbth  6777  fientri3  6803  unsnfidcex  6808  undifdc  6812  iunfidisj  6834  fiuni  6866  ordiso2  6920  acfun  7063  ccfunen  7079  addcmpblnq  7175  mulcmpblnq  7176  ordpipqqs  7182  addcmpblnq0  7251  mulcmpblnq0  7252  prml  7285  addlocpr  7344  prmuloc  7374  mullocpr  7379  ltexprlemopl  7409  ltexprlemopu  7411  ltexprlemloc  7415  ltexprlemrl  7418  ltexprlemru  7420  addcanprleml  7422  addcanprlemu  7423  aptiprleml  7447  ltmprr  7450  cauappcvgprlemopl  7454  cauappcvgprlemopu  7456  cauappcvgprlemloc  7460  caucvgprlemopl  7477  caucvgprlemopu  7479  caucvgprlemloc  7483  caucvgprprlemopu  7507  caucvgprprlemloc  7511  caucvgprprlemexbt  7514  caucvgprprlemaddq  7516  suplocexprlemrl  7525  suplocexprlemdisj  7528  suplocexprlemloc  7529  suplocexprlemub  7531  addcmpblnr  7547  mulcmpblnrlemg  7548  mulcmpblnr  7549  ltsrprg  7555  mulgt0sr  7586  caucvgsrlemgt1  7603  suplocsrlemb  7614  axmulcl  7674  axcaucvglemres  7707  axpre-suploclemres  7709  axpre-suploc  7710  cnegexlem1  7937  negeu  7953  add20  8236  apreap  8349  cru  8364  apsym  8368  apcotr  8369  apadd1  8370  apneg  8373  mulext1  8374  mulge0  8381  mulap0  8415  divdivdivap  8473  prodgt0  8610  ltmul12a  8618  lt2mul2div  8637  ledivdiv  8648  lediv12a  8652  qapne  9431  xleadd1a  9656  ixxss12  9689  elfz0ubfz0  9902  qtri3or  10020  exbtwnzlemstep  10025  exbtwnzlemex  10027  exbtwnz  10028  rebtwn2zlemstep  10030  rebtwn2z  10032  btwnzge0  10073  iseqf1olemqf1o  10266  mulexpzap  10333  leexp1a  10348  hashen  10530  fihashdom  10549  hashun  10551  cjap  10678  cvg1nlemres  10757  rsqrmo  10799  abslt  10860  abs3lem  10883  cau3lem  10886  rexanre  10992  xrmaxltsup  11027  climcau  11116  sumeq2  11128  summodc  11152  fisumss  11161  fsum2d  11204  fsumabs  11234  fsumiun  11246  prodeq2  11326  prodmodclem2  11346  eirrap  11484  divalglemeunn  11618  divalglemeuneg  11620  bezoutlemnewy  11684  bezoutlemstep  11685  bezoutlemmain  11686  bezoutlembi  11693  bezoutlemeu  11695  qredeu  11778  pw2dvdseu  11846  sqrt2irrap  11858  ennnfonelemg  11916  ennnfonelemrnh  11929  ctiunctlemfo  11952  restbasg  12337  cnpnei  12388  cnptoprest2  12409  cnpdis  12411  lmtopcnp  12419  txcnp  12440  ismet2  12523  blininf  12593  metss2lem  12666  xmettxlem  12678  xmettx  12679  metcnp  12681  metcnpi3  12686  addcncntoplem  12720  fsumcncntop  12725  mulc1cncf  12745  cncfco  12747  mulcncf  12760  dedekindeulemuub  12764  dedekindeu  12770  dedekindicclemuub  12773  ivthinclemloc  12788  ivthinc  12790  limcimo  12803  limccnp2cntop  12815  dveflem  12855  qdencn  13222