ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad3antrrr GIF version

Theorem ad3antrrr 469
Description: Deduction adding three conjuncts to antecedent. (Contributed by NM, 28-Jul-2012.)
Hypothesis
Ref Expression
ad2ant.1 (𝜑𝜓)
Assertion
Ref Expression
ad3antrrr ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)

Proof of Theorem ad3antrrr
StepHypRef Expression
1 ad2ant.1 . . 3 (𝜑𝜓)
21adantr 265 . 2 ((𝜑𝜒) → 𝜓)
32ad2antrr 465 1 ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem is referenced by:  ad4antr  471  phplem4on  6359  ltaddpr  6752  ltexprlemrl  6765  addcanprleml  6769  addcanprlemu  6770  aptiprleml  6794  aptiprlemu  6795  cauappcvgprlemdisj  6806  cauappcvgprlemladdrl  6812  caucvgprlemloc  6830  caucvgprlemladdrl  6833  caucvgprprlemopl  6852  caucvgprprlemloc  6858  caucvgprprlemexbt  6861  caucvgsrlemoffres  6941  axcaucvglemcau  7029  axcaucvglemres  7030  apreim  7667  apsym  7670  apcotr  7671  apadd1  7672  apneg  7675  mulext1  7676  mulge0  7683  apti  7686  qapne  8670  qtri3or  9199  qbtwnzlemstep  9204  rebtwn2zlemstep  9208  addmodlteq  9347  faclbnd  9608  cvg1nlemres  9811  resqrexlemoverl  9847  resqrexlemglsq  9848  resqrexlemga  9849  climrecvg1n  10097  serif0  10101  dvds2ln  10139
  Copyright terms: Public domain W3C validator