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

Theorem ad2ant2rl 468
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 24-Nov-2007.)
Hypothesis
Ref Expression
ad2ant2.1 ((φ ψ) → χ)
Assertion
Ref Expression
ad2ant2rl (((φ θ) (τ ψ)) → χ)

Proof of Theorem ad2ant2rl
StepHypRef Expression
1 ad2ant2.1 . . 3 ((φ ψ) → χ)
21adantrl 450 . 2 ((φ (τ ψ)) → χ)
32adantlr 449 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:  fvtp1g  5290  fcof1o  5350  addcomnqg  6234  addassnqg  6235  nqtri3or  6249  ltexnqq  6260  nqnq0pi  6287  nqpnq0nq  6302  nqnq0a  6303  addassnq0lemcl  6310  ltaddpr  6428  ltexprlemloc  6438  addcanprlemu  6446  recexprlem1ssu  6462  aptiprleml  6467  mulcomsrg  6501  mulasssrg  6502  distrsrg  6503  aptisr  6521  mulcnsr  6545  cnegex  6791  muladd  6982
  Copyright terms: Public domain W3C validator