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

Theorem ad2ant2l 492
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
ad2ant2.1  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
ad2ant2l  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  ch )

Proof of Theorem ad2ant2l
StepHypRef Expression
1 ad2ant2.1 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
21adantrl 462 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantll 460 1  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem is referenced by:  mpteqb  5293  mpt2fun  5634  xpdom2  6375  addcmpblnq  6619  addpipqqslem  6621  addpipqqs  6622  addclnq  6627  addcomnqg  6633  addassnqg  6634  mulcomnqg  6635  mulassnqg  6636  distrnqg  6639  ltdcnq  6649  enq0ref  6685  addcmpblnq0  6695  addclnq0  6703  nqpnq0nq  6705  nqnq0a  6706  nqnq0m  6707  distrnq0  6711  mulcomnq0  6712  addassnq0lemcl  6713  genpdisj  6775  appdiv0nq  6816  addcomsrg  6994  mulcomsrg  6996  mulasssrg  6997  distrsrg  6998  addcnsr  7064  mulcnsr  7065  addcnsrec  7072  axaddcl  7094  axmulcl  7096  axaddcom  7098  add42  7337  muladd  7555  mulsub  7572  apreim  7770  divmuleqap  7872  ltmul12a  8005  lemul12b  8006  lemul12a  8007  qaddcl  8801  qmulcl  8803  iooshf  9051  fzass4  9156  elfzomelpfzo  9317
  Copyright terms: Public domain W3C validator