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

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

Proof of Theorem ad2ant2lr
StepHypRef Expression
1 ad2ant2.1 . . 3 ((φ ψ) → χ)
21adantrr 448 . 2 ((φ (ψ τ)) → χ)
32adantll 445 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:  mpteqb  5204  addcomnqg  6365  addassnqg  6366  nqtri3or  6380  lt2addnq  6388  enq0ref  6415  enq0tr  6416  nqnq0pi  6420  nqpnq0nq  6435  nqnq0a  6436  distrnq0  6441  addassnq0lemcl  6443  ltsrprg  6635  mulcomsrg  6645  mulasssrg  6646  distrsrg  6647  aptisr  6665  mulcnsr  6692  cnegex  6946  sub4  7012  muladd  7137  ltleadd  7196  divdivdivap  7431  divadddivap  7445  ltmul12a  7567  fzrev  8676
  Copyright terms: Public domain W3C validator