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  5872  tfrlemisucaccv  6418  tfr1onlemsucaccv  6434  tfrcllemsucaccv  6447  addcmpblnq  7487  mulcmpblnq  7488  ordpipqqs  7494  nqnq0pi  7558  addcmpblnq0  7563  mulcmpblnq0  7564  addnq0mo  7567  mulnq0mo  7568  prarloclemcalc  7622  prarloc  7623  nqprl  7671  mullocpr  7691  distrlem4prl  7704  distrlem4pru  7705  ltprordil  7709  ltexprlemlol  7722  ltexprlemopu  7723  ltexprlemupu  7724  ltexprlemru  7732  cauappcvgprlemopl  7766  cauappcvgprlem2  7780  caucvgprlemopl  7789  caucvgprlem2  7800  caucvgprprlemexbt  7826  caucvgprprlem2  7830  suplocexprlemloc  7841  suplocexprlemub  7843  suplocexprlemlub  7844  addcmpblnr  7859  mulcmpblnrlemg  7860  mulcmpblnr  7861  prsrlem1  7862  addsrmo  7863  mulsrmo  7864  ltsrprg  7867  axmulcl  7986  recriota  8010  ltmul1  8672  divdivdivap  8793  divsubdivap  8808  ledivdiv  8970  lediv12a  8974  suprzcl2dc  10389  exbtwnz  10400  qbtwnre  10406  ioom  10410  seq3caopr  10647  seqcaoprg  10648  leexp2r  10745  hashunlem  10956  recvguniq  11350  rsqrmo  11382  fsum2dlemstep  11789  expcnvre  11858  fprod2dlemstep  11977  bezout  12376  qredeu  12463  pw2dvdseu  12534  oddpwdclemndvds  12537  pcqmul  12670  pcadd  12707  pockthg  12724  grprida  13263  ghmpreima  13646  unitgrp  13922  islmodd  14099  lmodprop2d  14154  lsspropdg  14237  epttop  14606  restbasg  14684  iscnp4  14734  cnptopco  14738  blssps  14943  blss  14944  metequiv2  15012  xmetxpbl  15024  suplociccex  15141  dedekindicc  15149  limcimolemlt  15180  lgsquad2lem2  15603  2sqlem5  15640  2omap  16006