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  5839  tfrlemisucaccv  6378  tfr1onlemsucaccv  6394  tfrcllemsucaccv  6407  addcmpblnq  7427  mulcmpblnq  7428  ordpipqqs  7434  nqnq0pi  7498  addcmpblnq0  7503  mulcmpblnq0  7504  addnq0mo  7507  mulnq0mo  7508  prarloclemcalc  7562  prarloc  7563  nqprl  7611  mullocpr  7631  distrlem4prl  7644  distrlem4pru  7645  ltprordil  7649  ltexprlemlol  7662  ltexprlemopu  7663  ltexprlemupu  7664  ltexprlemru  7672  cauappcvgprlemopl  7706  cauappcvgprlem2  7720  caucvgprlemopl  7729  caucvgprlem2  7740  caucvgprprlemexbt  7766  caucvgprprlem2  7770  suplocexprlemloc  7781  suplocexprlemub  7783  suplocexprlemlub  7784  addcmpblnr  7799  mulcmpblnrlemg  7800  mulcmpblnr  7801  prsrlem1  7802  addsrmo  7803  mulsrmo  7804  ltsrprg  7807  axmulcl  7926  recriota  7950  ltmul1  8611  divdivdivap  8732  divsubdivap  8747  ledivdiv  8909  lediv12a  8913  exbtwnz  10319  qbtwnre  10325  ioom  10329  seq3caopr  10566  seqcaoprg  10567  leexp2r  10664  hashunlem  10875  recvguniq  11139  rsqrmo  11171  fsum2dlemstep  11577  expcnvre  11646  fprod2dlemstep  11765  suprzcl2dc  12092  bezout  12148  qredeu  12235  pw2dvdseu  12306  oddpwdclemndvds  12309  pcqmul  12441  pcadd  12478  pockthg  12495  grprida  12970  ghmpreima  13336  unitgrp  13612  islmodd  13789  lmodprop2d  13844  lsspropdg  13927  epttop  14258  restbasg  14336  iscnp4  14386  cnptopco  14390  blssps  14595  blss  14596  metequiv2  14664  xmetxpbl  14676  suplociccex  14779  dedekindicc  14787  limcimolemlt  14818  2sqlem5  15206