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  5942  tfrlemisucaccv  6496  tfr1onlemsucaccv  6512  tfrcllemsucaccv  6525  addcmpblnq  7592  mulcmpblnq  7593  ordpipqqs  7599  nqnq0pi  7663  addcmpblnq0  7668  mulcmpblnq0  7669  addnq0mo  7672  mulnq0mo  7673  prarloclemcalc  7727  prarloc  7728  nqprl  7776  mullocpr  7796  distrlem4prl  7809  distrlem4pru  7810  ltprordil  7814  ltexprlemlol  7827  ltexprlemopu  7828  ltexprlemupu  7829  ltexprlemru  7837  cauappcvgprlemopl  7871  cauappcvgprlem2  7885  caucvgprlemopl  7894  caucvgprlem2  7905  caucvgprprlemexbt  7931  caucvgprprlem2  7935  suplocexprlemloc  7946  suplocexprlemub  7948  suplocexprlemlub  7949  addcmpblnr  7964  mulcmpblnrlemg  7965  mulcmpblnr  7966  prsrlem1  7967  addsrmo  7968  mulsrmo  7969  ltsrprg  7972  axmulcl  8091  recriota  8115  ltmul1  8777  divdivdivap  8898  divsubdivap  8913  ledivdiv  9075  lediv12a  9079  suprzcl2dc  10505  exbtwnz  10516  qbtwnre  10522  ioom  10526  seq3caopr  10763  seqcaoprg  10764  leexp2r  10861  hashunlem  11073  wrd2ind  11313  recvguniq  11578  rsqrmo  11610  fsum2dlemstep  12018  expcnvre  12087  fprod2dlemstep  12206  bezout  12605  qredeu  12692  pw2dvdseu  12763  oddpwdclemndvds  12766  pcqmul  12899  pcadd  12936  pockthg  12953  grprida  13493  ghmpreima  13876  unitgrp  14154  islmodd  14331  lmodprop2d  14386  lsspropdg  14469  epttop  14843  restbasg  14921  iscnp4  14971  cnptopco  14975  blssps  15180  blss  15181  metequiv2  15249  xmetxpbl  15261  suplociccex  15378  dedekindicc  15386  limcimolemlt  15417  lgsquad2lem2  15840  2sqlem5  15877  2omap  16654