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

Theorem ad3antrrr 461
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 261 . 2 ((𝜑𝜒) → 𝜓)
32ad2antrr 457 1 ((((𝜑𝜒) ∧ 𝜃) ∧ 𝜏) → 𝜓)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  ad4antr  463  phplem4on  6329  ltaddpr  6695  ltexprlemrl  6708  addcanprleml  6712  addcanprlemu  6713  aptiprleml  6737  aptiprlemu  6738  cauappcvgprlemdisj  6749  cauappcvgprlemladdrl  6755  caucvgprlemloc  6773  caucvgprlemladdrl  6776  caucvgprprlemopl  6795  caucvgprprlemloc  6801  caucvgprprlemexbt  6804  caucvgsrlemoffres  6884  axcaucvglemcau  6972  axcaucvglemres  6973  apreim  7594  apsym  7597  apcotr  7598  apadd1  7599  apneg  7602  mulext1  7603  mulge0  7610  apti  7613  qapne  8574  qtri3or  9098  qbtwnzlemstep  9103  rebtwn2zlemstep  9107  cvg1nlemres  9584  resqrexlemoverl  9619  resqrexlemglsq  9620  resqrexlemga  9621  climrecvg1n  9867  serif0  9871
  Copyright terms: Public domain W3C validator