Theorem simprrr 540

Description: Simplification of a conjunction. (Contributed by Jeff Hankins, 28-Jul-2009.)

Assertion

Ref	Expression
simprrr	⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

Proof of Theorem simprrr

Step	Hyp	Ref	Expression
1		simpr 110	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 491	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:  fliftfun  5846  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  addcmpblnq  7451  mulcmpblnq  7452  ordpipqqs  7458  nqnq0pi  7522  addcmpblnq0  7527  mulcmpblnq0  7528  addnq0mo  7531  mulnq0mo  7532  prarloclemcalc  7586  prarloc  7587  nqprl  7635  mullocpr  7655  distrlem4prl  7668  distrlem4pru  7669  ltprordil  7673  ltexprlemlol  7686  ltexprlemopu  7687  ltexprlemupu  7688  ltexprlemru  7696  cauappcvgprlemopl  7730  cauappcvgprlem2  7744  caucvgprlemopl  7753  caucvgprlem2  7764  caucvgprprlemexbt  7790  caucvgprprlem2  7794  suplocexprlemloc  7805  suplocexprlemub  7807  suplocexprlemlub  7808  addcmpblnr  7823  mulcmpblnrlemg  7824  mulcmpblnr  7825  prsrlem1  7826  addsrmo  7827  mulsrmo  7828  ltsrprg  7831  axmulcl  7950  recriota  7974  ltmul1  8636  divdivdivap  8757  divsubdivap  8772  ledivdiv  8934  lediv12a  8938  suprzcl2dc  10346  exbtwnz  10357  qbtwnre  10363  ioom  10367  seq3caopr  10604  seqcaoprg  10605  leexp2r  10702  hashunlem  10913  recvguniq  11177  rsqrmo  11209  fsum2dlemstep  11616  expcnvre  11685  fprod2dlemstep  11804  bezout  12203  qredeu  12290  pw2dvdseu  12361  oddpwdclemndvds  12364  pcqmul  12497  pcadd  12534  pockthg  12551  grprida  13089  ghmpreima  13472  unitgrp  13748  islmodd  13925  lmodprop2d  13980  lsspropdg  14063  epttop  14410  restbasg  14488  iscnp4  14538  cnptopco  14542  blssps  14747  blss  14748  metequiv2  14816  xmetxpbl  14828  suplociccex  14945  dedekindicc  14953  limcimolemlt  14984  lgsquad2lem2  15407  2sqlem5  15444  2omap  15726