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  5312  fcof1o  5372  addcomnqg  6365  addassnqg  6366  nqtri3or  6380  ltexnqq  6391  nqnq0pi  6420  nqpnq0nq  6435  nqnq0a  6436  addassnq0lemcl  6443  ltaddpr  6569  ltexprlemloc  6579  addcanprlemu  6587  recexprlem1ssu  6604  aptiprleml  6609  mulcomsrg  6645  mulasssrg  6646  distrsrg  6647  aptisr  6665  mulcnsr  6692  cnegex  6946  muladd  7137  lemul12b  7568  qaddcl  8306  iooshf  8551  elfzomelpfzo  8817  expnegzap  8903
  Copyright terms: Public domain W3C validator