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

Theorem ad2ant2l 499
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 469 . 2  |-  ( (
ph  /\  ( ta  /\ 
ps ) )  ->  ch )
32adantll 467 1  |-  ( ( ( th  /\  ph )  /\  ( ta  /\  ps ) )  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  mpteqb  5479  mpofun  5841  xpdom2  6693  addcmpblnq  7143  addpipqqslem  7145  addpipqqs  7146  addclnq  7151  addcomnqg  7157  addassnqg  7158  mulcomnqg  7159  mulassnqg  7160  distrnqg  7163  ltdcnq  7173  enq0ref  7209  addcmpblnq0  7219  addclnq0  7227  nqpnq0nq  7229  nqnq0a  7230  nqnq0m  7231  distrnq0  7235  mulcomnq0  7236  addassnq0lemcl  7237  genpdisj  7299  appdiv0nq  7340  addcomsrg  7531  mulcomsrg  7533  mulasssrg  7534  distrsrg  7535  addcnsr  7610  mulcnsr  7611  addcnsrec  7618  axaddcl  7640  axmulcl  7642  axaddcom  7646  add42  7892  muladd  8114  mulsub  8131  apreim  8333  divmuleqap  8445  ltmul12a  8586  lemul12b  8587  lemul12a  8588  qaddcl  9395  qmulcl  9397  iooshf  9703  fzass4  9810  elfzomelpfzo  9976  tanaddaplem  11372  opnneissb  12251  neitx  12364  txcnmpt  12369  txrest  12372  metcnp3  12607  cncfmet  12675  dveflem  12782
  Copyright terms: Public domain W3C validator