ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ad2ant2lr 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  6416  enq0tr  6417  nqnq0pi  6421  nqpnq0nq  6436  nqnq0a  6437  distrnq0  6442  addassnq0lemcl  6444  ltsrprg  6675  mulcomsrg  6685  mulasssrg  6686  distrsrg  6687  aptisr  6705  mulcnsr  6732  cnegex  6986  sub4  7052  muladd  7177  ltleadd  7236  divdivdivap  7471  divadddivap  7485  ltmul12a  7607  fzrev  8716
  Copyright terms: Public domain W3C validator