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

Theorem ad2ant2l 477
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 447 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantll 445 1  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  ch )
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  5261  mpt2fun  5603  xpdom2  6305  addcmpblnq  6465  addpipqqslem  6467  addpipqqs  6468  addclnq  6473  addcomnqg  6479  addassnqg  6480  mulcomnqg  6481  mulassnqg  6482  distrnqg  6485  ltdcnq  6495  enq0ref  6531  addcmpblnq0  6541  addclnq0  6549  nqpnq0nq  6551  nqnq0a  6552  nqnq0m  6553  distrnq0  6557  mulcomnq0  6558  addassnq0lemcl  6559  genpdisj  6621  appdiv0nq  6662  addcomsrg  6840  mulcomsrg  6842  mulasssrg  6843  distrsrg  6844  addcnsr  6910  mulcnsr  6911  addcnsrec  6918  axaddcl  6940  axmulcl  6942  axaddcom  6944  add42  7173  muladd  7381  mulsub  7398  apreim  7594  divmuleqap  7693  ltmul12a  7826  lemul12b  7827  lemul12a  7828  qaddcl  8570  qmulcl  8572  iooshf  8821  fzass4  8925  elfzomelpfzo  9087
  Copyright terms: Public domain W3C validator