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  5202  mpt2fun  5542  xpdom2  6234  addcmpblnq  6344  addpipqqslem  6346  addpipqqs  6347  addclnq  6352  addcomnqg  6358  addassnqg  6359  mulcomnqg  6360  mulassnqg  6361  distrnqg  6364  ltdcnq  6374  enq0ref  6408  addcmpblnq0  6418  addclnq0  6426  nqpnq0nq  6428  nqnq0a  6429  nqnq0m  6430  distrnq0  6434  mulcomnq0  6435  addassnq0lemcl  6436  genpdisj  6499  appdiv0nq  6535  addcomsrg  6635  mulcomsrg  6637  mulasssrg  6638  distrsrg  6639  addcnsr  6683  mulcnsr  6684  addcnsrec  6691  axaddcl  6702  axmulcl  6704  axaddcom  6706  add42  6922  muladd  7129  mulsub  7146  apreim  7339  divmuleqap  7427  ltmul12a  7558  lemul12b  7559  lemul12a  7560  qaddcl  8295  qmulcl  8297  iooshf  8539  fzass4  8641  elfzomelpfzo  8803
  Copyright terms: Public domain W3C validator