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

Theorem ad2ant2l 508
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 478 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantll 476 1  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem is referenced by:  mpteqb  5601  mpofun  5970  xpdom2  6824  addcmpblnq  7344  addpipqqslem  7346  addpipqqs  7347  addclnq  7352  addcomnqg  7358  addassnqg  7359  mulcomnqg  7360  mulassnqg  7361  distrnqg  7364  ltdcnq  7374  enq0ref  7410  addcmpblnq0  7420  addclnq0  7428  nqpnq0nq  7430  nqnq0a  7431  nqnq0m  7432  distrnq0  7436  mulcomnq0  7437  addassnq0lemcl  7438  genpdisj  7500  appdiv0nq  7541  addcomsrg  7732  mulcomsrg  7734  mulasssrg  7735  distrsrg  7736  addcnsr  7811  mulcnsr  7812  addcnsrec  7819  axaddcl  7841  axmulcl  7843  axaddcom  7847  add42  8096  muladd  8318  mulsub  8335  apreim  8537  divmuleqap  8650  ltmul12a  8793  lemul12b  8794  lemul12a  8795  qaddcl  9611  qmulcl  9613  iooshf  9926  fzass4  10035  elfzomelpfzo  10204  tanaddaplem  11717  opnneissb  13288  neitx  13401  txcnmpt  13406  txrest  13409  metcnp3  13644  cncfmet  13712  dveflem  13820  lgsdir2  14067
  Copyright terms: Public domain W3C validator