Theorem simprrr 530

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 109	. 2 ⊢ ((𝜒 ∧ 𝜃) → 𝜃)
2	1	ad2antll 483	1 ⊢ ((𝜑 ∧ (𝜓 ∧ (𝜒 ∧ 𝜃))) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem is referenced by:  fliftfun  5764  tfrlemisucaccv  6293  tfr1onlemsucaccv  6309  tfrcllemsucaccv  6322  addcmpblnq  7308  mulcmpblnq  7309  ordpipqqs  7315  nqnq0pi  7379  addcmpblnq0  7384  mulcmpblnq0  7385  addnq0mo  7388  mulnq0mo  7389  prarloclemcalc  7443  prarloc  7444  nqprl  7492  mullocpr  7512  distrlem4prl  7525  distrlem4pru  7526  ltprordil  7530  ltexprlemlol  7543  ltexprlemopu  7544  ltexprlemupu  7545  ltexprlemru  7553  cauappcvgprlemopl  7587  cauappcvgprlem2  7601  caucvgprlemopl  7610  caucvgprlem2  7621  caucvgprprlemexbt  7647  caucvgprprlem2  7651  suplocexprlemloc  7662  suplocexprlemub  7664  suplocexprlemlub  7665  addcmpblnr  7680  mulcmpblnrlemg  7681  mulcmpblnr  7682  prsrlem1  7683  addsrmo  7684  mulsrmo  7685  ltsrprg  7688  axmulcl  7807  recriota  7831  ltmul1  8490  divdivdivap  8609  divsubdivap  8624  ledivdiv  8785  lediv12a  8789  exbtwnz  10186  qbtwnre  10192  ioom  10196  seq3caopr  10418  leexp2r  10509  hashunlem  10717  recvguniq  10937  rsqrmo  10969  fsum2dlemstep  11375  expcnvre  11444  fprod2dlemstep  11563  suprzcl2dc  11888  bezout  11944  qredeu  12029  pw2dvdseu  12100  oddpwdclemndvds  12103  pcqmul  12235  pcadd  12271  pockthg  12287  grpridd  12618  epttop  12730  restbasg  12808  iscnp4  12858  cnptopco  12862  blssps  13067  blss  13068  metequiv2  13136  xmetxpbl  13148  suplociccex  13243  dedekindicc  13251  limcimolemlt  13273  2sqlem5  13595