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

Theorem ad2ant2l 477
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1 ((φ ψ) → χ)
Assertion
Ref Expression
ad2ant2l (((θ φ) (τ ψ)) → χ)

Proof of Theorem ad2ant2l
StepHypRef Expression
1 ad2ant2.1 . . 3 ((φ ψ) → χ)
21adantrl 447 . 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  mpt2fun  5545  xpdom2  6241  addcmpblnq  6351  addpipqqslem  6353  addpipqqs  6354  addclnq  6359  addcomnqg  6365  addassnqg  6366  mulcomnqg  6367  mulassnqg  6368  distrnqg  6371  ltdcnq  6381  enq0ref  6415  addcmpblnq0  6425  addclnq0  6433  nqpnq0nq  6435  nqnq0a  6436  nqnq0m  6437  distrnq0  6441  mulcomnq0  6442  addassnq0lemcl  6443  genpdisj  6506  appdiv0nq  6543  addcomsrg  6643  mulcomsrg  6645  mulasssrg  6646  distrsrg  6647  addcnsr  6691  mulcnsr  6692  addcnsrec  6699  axaddcl  6710  axmulcl  6712  axaddcom  6714  add42  6930  muladd  7137  mulsub  7154  apreim  7347  divmuleqap  7435  ltmul12a  7567  lemul12b  7568  lemul12a  7569  qaddcl  8306  qmulcl  8308  iooshf  8551  fzass4  8655  elfzomelpfzo  8817
  Copyright terms: Public domain W3C validator