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  5947  tfrlemisucaccv  6534  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  addcmpblnq  7630  mulcmpblnq  7631  ordpipqqs  7637  nqnq0pi  7701  addcmpblnq0  7706  mulcmpblnq0  7707  addnq0mo  7710  mulnq0mo  7711  prarloclemcalc  7765  prarloc  7766  nqprl  7814  mullocpr  7834  distrlem4prl  7847  distrlem4pru  7848  ltprordil  7852  ltexprlemlol  7865  ltexprlemopu  7866  ltexprlemupu  7867  ltexprlemru  7875  cauappcvgprlemopl  7909  cauappcvgprlem2  7923  caucvgprlemopl  7932  caucvgprlem2  7943  caucvgprprlemexbt  7969  caucvgprprlem2  7973  suplocexprlemloc  7984  suplocexprlemub  7986  suplocexprlemlub  7987  addcmpblnr  8002  mulcmpblnrlemg  8003  mulcmpblnr  8004  prsrlem1  8005  addsrmo  8006  mulsrmo  8007  ltsrprg  8010  axmulcl  8129  recriota  8153  ltmul1  8814  divdivdivap  8935  divsubdivap  8950  ledivdiv  9112  lediv12a  9116  suprzcl2dc  10545  exbtwnz  10556  qbtwnre  10562  ioom  10566  seq3caopr  10803  seqcaoprg  10804  leexp2r  10901  hashunlem  11113  wrd2ind  11353  recvguniq  11618  rsqrmo  11650  fsum2dlemstep  12058  expcnvre  12127  fprod2dlemstep  12246  bezout  12645  qredeu  12732  pw2dvdseu  12803  oddpwdclemndvds  12806  pcqmul  12939  pcadd  12976  pockthg  12993  grprida  13533  ghmpreima  13916  unitgrp  14194  islmodd  14372  lmodprop2d  14427  lsspropdg  14510  epttop  14884  restbasg  14962  iscnp4  15012  cnptopco  15016  blssps  15221  blss  15222  metequiv2  15290  xmetxpbl  15302  suplociccex  15419  dedekindicc  15427  limcimolemlt  15458  pellexlem3  15776  lgsquad2lem2  15884  2sqlem5  15921  2omap  16698