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

Theorem ad2ant2rl 480
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 447 . 2 ((φ (τ ψ)) → χ)
32adantlr 446 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  5312  fcof1o  5372  addcomnqg  6365  addassnqg  6366  nqtri3or  6380  ltexnqq  6391  nqnq0pi  6421  nqpnq0nq  6436  nqnq0a  6437  addassnq0lemcl  6444  ltaddpr  6571  ltexprlemloc  6581  addcanprlemu  6589  recexprlem1ssu  6606  aptiprleml  6611  mulcomsrg  6685  mulasssrg  6686  distrsrg  6687  aptisr  6705  mulcnsr  6732  cnegex  6986  muladd  7177  lemul12b  7608  qaddcl  8346  iooshf  8591  elfzomelpfzo  8857  expnegzap  8943
  Copyright terms: Public domain W3C validator