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  5975  tfrlemisucaccv  6569  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  2omap  7282  addcmpblnq  7698  mulcmpblnq  7699  ordpipqqs  7705  nqnq0pi  7769  addcmpblnq0  7774  mulcmpblnq0  7775  addnq0mo  7778  mulnq0mo  7779  prarloclemcalc  7833  prarloc  7834  nqprl  7882  mullocpr  7902  distrlem4prl  7915  distrlem4pru  7916  ltprordil  7920  ltexprlemlol  7933  ltexprlemopu  7934  ltexprlemupu  7935  ltexprlemru  7943  cauappcvgprlemopl  7977  cauappcvgprlem2  7991  caucvgprlemopl  8000  caucvgprlem2  8011  caucvgprprlemexbt  8037  caucvgprprlem2  8041  suplocexprlemloc  8052  suplocexprlemub  8054  suplocexprlemlub  8055  addcmpblnr  8070  mulcmpblnrlemg  8071  mulcmpblnr  8072  prsrlem1  8073  addsrmo  8074  mulsrmo  8075  ltsrprg  8078  axmulcl  8197  recriota  8221  ltmul1  8884  divdivdivap  9007  divsubdivap  9022  ledivdiv  9184  lediv12a  9188  infssfzcldc  10621  infssfzledc  10622  suprzcl2dc  10626  exbtwnz  10637  qbtwnre  10643  ioom  10647  seq3caopr  10884  seqcaoprg  10885  leexp2r  10982  hashunlem  11196  hashfibclem  11234  wrd2ind  11443  recvguniq  11708  rsqrmo  11740  fsum2dlemstep  12148  expcnvre  12217  fprod2dlemstep  12336  bezout  12735  qredeu  12822  pw2dvdseu  12893  oddpwdclemndvds  12896  pcqmul  13029  pcadd  13066  pockthg  13083  grprida  13653  ghmpreima  14022  unitgrp  14364  islmodd  14570  lmodprop2d  14625  lsspropdg  14708  epttop  15084  restbasg  15162  iscnp4  15212  cnptopco  15216  blssps  15421  blss  15422  metequiv2  15490  xmetxpbl  15502  suplociccex  15619  dedekindicc  15627  limcimolemlt  15658  pellexlem3  15976  lgsquad2lem2  16084  2sqlem5  16121