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  5937  tfrlemisucaccv  6491  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  addcmpblnq  7587  mulcmpblnq  7588  ordpipqqs  7594  nqnq0pi  7658  addcmpblnq0  7663  mulcmpblnq0  7664  addnq0mo  7667  mulnq0mo  7668  prarloclemcalc  7722  prarloc  7723  nqprl  7771  mullocpr  7791  distrlem4prl  7804  distrlem4pru  7805  ltprordil  7809  ltexprlemlol  7822  ltexprlemopu  7823  ltexprlemupu  7824  ltexprlemru  7832  cauappcvgprlemopl  7866  cauappcvgprlem2  7880  caucvgprlemopl  7889  caucvgprlem2  7900  caucvgprprlemexbt  7926  caucvgprprlem2  7930  suplocexprlemloc  7941  suplocexprlemub  7943  suplocexprlemlub  7944  addcmpblnr  7959  mulcmpblnrlemg  7960  mulcmpblnr  7961  prsrlem1  7962  addsrmo  7963  mulsrmo  7964  ltsrprg  7967  axmulcl  8086  recriota  8110  ltmul1  8772  divdivdivap  8893  divsubdivap  8908  ledivdiv  9070  lediv12a  9074  suprzcl2dc  10500  exbtwnz  10511  qbtwnre  10517  ioom  10521  seq3caopr  10758  seqcaoprg  10759  leexp2r  10856  hashunlem  11068  wrd2ind  11305  recvguniq  11557  rsqrmo  11589  fsum2dlemstep  11997  expcnvre  12066  fprod2dlemstep  12185  bezout  12584  qredeu  12671  pw2dvdseu  12742  oddpwdclemndvds  12745  pcqmul  12878  pcadd  12915  pockthg  12932  grprida  13472  ghmpreima  13855  unitgrp  14133  islmodd  14310  lmodprop2d  14365  lsspropdg  14448  epttop  14817  restbasg  14895  iscnp4  14945  cnptopco  14949  blssps  15154  blss  15155  metequiv2  15223  xmetxpbl  15235  suplociccex  15352  dedekindicc  15360  limcimolemlt  15391  lgsquad2lem2  15814  2sqlem5  15851  2omap  16615