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  6416  addcmpblnq0  6426  addclnq0  6434  nqpnq0nq  6436  nqnq0a  6437  nqnq0m  6438  distrnq0  6442  mulcomnq0  6443  addassnq0lemcl  6444  genpdisj  6506  appdiv0nq  6545  addcomsrg  6683  mulcomsrg  6685  mulasssrg  6686  distrsrg  6687  addcnsr  6731  mulcnsr  6732  addcnsrec  6739  axaddcl  6750  axmulcl  6752  axaddcom  6754  add42  6970  muladd  7177  mulsub  7194  apreim  7387  divmuleqap  7475  ltmul12a  7607  lemul12b  7608  lemul12a  7609  qaddcl  8346  qmulcl  8348  iooshf  8591  fzass4  8695  elfzomelpfzo  8857
  Copyright terms: Public domain W3C validator