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  5843  tfrlemisucaccv  6383  tfr1onlemsucaccv  6399  tfrcllemsucaccv  6412  addcmpblnq  7434  mulcmpblnq  7435  ordpipqqs  7441  nqnq0pi  7505  addcmpblnq0  7510  mulcmpblnq0  7511  addnq0mo  7514  mulnq0mo  7515  prarloclemcalc  7569  prarloc  7570  nqprl  7618  mullocpr  7638  distrlem4prl  7651  distrlem4pru  7652  ltprordil  7656  ltexprlemlol  7669  ltexprlemopu  7670  ltexprlemupu  7671  ltexprlemru  7679  cauappcvgprlemopl  7713  cauappcvgprlem2  7727  caucvgprlemopl  7736  caucvgprlem2  7747  caucvgprprlemexbt  7773  caucvgprprlem2  7777  suplocexprlemloc  7788  suplocexprlemub  7790  suplocexprlemlub  7791  addcmpblnr  7806  mulcmpblnrlemg  7807  mulcmpblnr  7808  prsrlem1  7809  addsrmo  7810  mulsrmo  7811  ltsrprg  7814  axmulcl  7933  recriota  7957  ltmul1  8619  divdivdivap  8740  divsubdivap  8755  ledivdiv  8917  lediv12a  8921  suprzcl2dc  10329  exbtwnz  10340  qbtwnre  10346  ioom  10350  seq3caopr  10587  seqcaoprg  10588  leexp2r  10685  hashunlem  10896  recvguniq  11160  rsqrmo  11192  fsum2dlemstep  11599  expcnvre  11668  fprod2dlemstep  11787  bezout  12178  qredeu  12265  pw2dvdseu  12336  oddpwdclemndvds  12339  pcqmul  12472  pcadd  12509  pockthg  12526  grprida  13030  ghmpreima  13396  unitgrp  13672  islmodd  13849  lmodprop2d  13904  lsspropdg  13987  epttop  14326  restbasg  14404  iscnp4  14454  cnptopco  14458  blssps  14663  blss  14664  metequiv2  14732  xmetxpbl  14744  suplociccex  14861  dedekindicc  14869  limcimolemlt  14900  lgsquad2lem2  15323  2sqlem5  15360