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  5787  tfrlemisucaccv  6316  tfr1onlemsucaccv  6332  tfrcllemsucaccv  6345  addcmpblnq  7341  mulcmpblnq  7342  ordpipqqs  7348  nqnq0pi  7412  addcmpblnq0  7417  mulcmpblnq0  7418  addnq0mo  7421  mulnq0mo  7422  prarloclemcalc  7476  prarloc  7477  nqprl  7525  mullocpr  7545  distrlem4prl  7558  distrlem4pru  7559  ltprordil  7563  ltexprlemlol  7576  ltexprlemopu  7577  ltexprlemupu  7578  ltexprlemru  7586  cauappcvgprlemopl  7620  cauappcvgprlem2  7634  caucvgprlemopl  7643  caucvgprlem2  7654  caucvgprprlemexbt  7680  caucvgprprlem2  7684  suplocexprlemloc  7695  suplocexprlemub  7697  suplocexprlemlub  7698  addcmpblnr  7713  mulcmpblnrlemg  7714  mulcmpblnr  7715  prsrlem1  7716  addsrmo  7717  mulsrmo  7718  ltsrprg  7721  axmulcl  7840  recriota  7864  ltmul1  8523  divdivdivap  8643  divsubdivap  8658  ledivdiv  8820  lediv12a  8824  exbtwnz  10221  qbtwnre  10227  ioom  10231  seq3caopr  10453  leexp2r  10544  hashunlem  10752  recvguniq  10972  rsqrmo  11004  fsum2dlemstep  11410  expcnvre  11479  fprod2dlemstep  11598  suprzcl2dc  11923  bezout  11979  qredeu  12064  pw2dvdseu  12135  oddpwdclemndvds  12138  pcqmul  12270  pcadd  12306  pockthg  12322  grpridd  12681  epttop  13170  restbasg  13248  iscnp4  13298  cnptopco  13302  blssps  13507  blss  13508  metequiv2  13576  xmetxpbl  13588  suplociccex  13683  dedekindicc  13691  limcimolemlt  13713  2sqlem5  14035