Theorem simprrr 542

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  5968  tfrlemisucaccv  6555  tfr1onlemsucaccv  6571  tfrcllemsucaccv  6584  2omap  7268  addcmpblnq  7678  mulcmpblnq  7679  ordpipqqs  7685  nqnq0pi  7749  addcmpblnq0  7754  mulcmpblnq0  7755  addnq0mo  7758  mulnq0mo  7759  prarloclemcalc  7813  prarloc  7814  nqprl  7862  mullocpr  7882  distrlem4prl  7895  distrlem4pru  7896  ltprordil  7900  ltexprlemlol  7913  ltexprlemopu  7914  ltexprlemupu  7915  ltexprlemru  7923  cauappcvgprlemopl  7957  cauappcvgprlem2  7971  caucvgprlemopl  7980  caucvgprlem2  7991  caucvgprprlemexbt  8017  caucvgprprlem2  8021  suplocexprlemloc  8032  suplocexprlemub  8034  suplocexprlemlub  8035  addcmpblnr  8050  mulcmpblnrlemg  8051  mulcmpblnr  8052  prsrlem1  8053  addsrmo  8054  mulsrmo  8055  ltsrprg  8058  axmulcl  8177  recriota  8201  ltmul1  8862  divdivdivap  8983  divsubdivap  8998  ledivdiv  9160  lediv12a  9164  suprzcl2dc  10595  exbtwnz  10606  qbtwnre  10612  ioom  10616  seq3caopr  10853  seqcaoprg  10854  leexp2r  10951  hashunlem  11163  hashfibclem  11199  wrd2ind  11408  recvguniq  11673  rsqrmo  11705  fsum2dlemstep  12113  expcnvre  12182  fprod2dlemstep  12301  bezout  12700  qredeu  12787  pw2dvdseu  12858  oddpwdclemndvds  12861  pcqmul  12994  pcadd  13031  pockthg  13048  grprida  13589  ghmpreima  13972  unitgrp  14250  islmodd  14428  lmodprop2d  14483  lsspropdg  14566  epttop  14942  restbasg  15020  iscnp4  15070  cnptopco  15074  blssps  15279  blss  15280  metequiv2  15348  xmetxpbl  15360  suplociccex  15477  dedekindicc  15485  limcimolemlt  15516  pellexlem3  15834  lgsquad2lem2  15942  2sqlem5  15979