ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad2ant2rl Structured version   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  5310  fcof1o  5370  addcomnqg  6358  addassnqg  6359  nqtri3or  6373  ltexnqq  6384  nqnq0pi  6413  nqpnq0nq  6428  nqnq0a  6429  addassnq0lemcl  6436  ltaddpr  6561  ltexprlemloc  6571  addcanprlemu  6579  recexprlem1ssu  6596  aptiprleml  6601  mulcomsrg  6637  mulasssrg  6638  distrsrg  6639  aptisr  6657  mulcnsr  6684  cnegex  6938  muladd  7129  lemul12b  7559  qaddcl  8295  iooshf  8539  elfzomelpfzo  8803
  Copyright terms: Public domain W3C validator