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  5846  tfrlemisucaccv  6392  tfr1onlemsucaccv  6408  tfrcllemsucaccv  6421  addcmpblnq  7453  mulcmpblnq  7454  ordpipqqs  7460  nqnq0pi  7524  addcmpblnq0  7529  mulcmpblnq0  7530  addnq0mo  7533  mulnq0mo  7534  prarloclemcalc  7588  prarloc  7589  nqprl  7637  mullocpr  7657  distrlem4prl  7670  distrlem4pru  7671  ltprordil  7675  ltexprlemlol  7688  ltexprlemopu  7689  ltexprlemupu  7690  ltexprlemru  7698  cauappcvgprlemopl  7732  cauappcvgprlem2  7746  caucvgprlemopl  7755  caucvgprlem2  7766  caucvgprprlemexbt  7792  caucvgprprlem2  7796  suplocexprlemloc  7807  suplocexprlemub  7809  suplocexprlemlub  7810  addcmpblnr  7825  mulcmpblnrlemg  7826  mulcmpblnr  7827  prsrlem1  7828  addsrmo  7829  mulsrmo  7830  ltsrprg  7833  axmulcl  7952  recriota  7976  ltmul1  8638  divdivdivap  8759  divsubdivap  8774  ledivdiv  8936  lediv12a  8940  suprzcl2dc  10348  exbtwnz  10359  qbtwnre  10365  ioom  10369  seq3caopr  10606  seqcaoprg  10607  leexp2r  10704  hashunlem  10915  recvguniq  11179  rsqrmo  11211  fsum2dlemstep  11618  expcnvre  11687  fprod2dlemstep  11806  bezout  12205  qredeu  12292  pw2dvdseu  12363  oddpwdclemndvds  12366  pcqmul  12499  pcadd  12536  pockthg  12553  grprida  13091  ghmpreima  13474  unitgrp  13750  islmodd  13927  lmodprop2d  13982  lsspropdg  14065  epttop  14412  restbasg  14490  iscnp4  14540  cnptopco  14544  blssps  14749  blss  14750  metequiv2  14818  xmetxpbl  14830  suplociccex  14947  dedekindicc  14955  limcimolemlt  14986  lgsquad2lem2  15409  2sqlem5  15446  2omap  15728