ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad3antrrr Structured version   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  ltaddpr  6571  ltexprlemrl  6584  addcanprleml  6588  addcanprlemu  6589  aptiprleml  6611  aptiprlemu  6612  cauappcvgprlemdisj  6623  cauappcvgprlemladdrl  6629  caucvgprlemloc  6646  caucvgprlemladdrl  6649  apreim  7387  apsym  7390  apcotr  7391  apadd1  7392  apneg  7395  mulext1  7396  mulge0  7403  apti  7406  qapne  8350
  Copyright terms: Public domain W3C validator