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

Theorem 3ad2antl1 1161
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)
Hypothesis
Ref Expression
3ad2antl.1  |-  ( (
ph  /\  ch )  ->  th )
Assertion
Ref Expression
3ad2antl1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )

Proof of Theorem 3ad2antl1
StepHypRef Expression
1 3ad2antl.1 . . 3  |-  ( (
ph  /\  ch )  ->  th )
21adantlr 477 . 2  |-  ( ( ( ph  /\  ta )  /\  ch )  ->  th )
323adantl2 1156 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 980
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 depends on definitions:  df-bi 117  df-3an 982
This theorem is referenced by:  acexmid  5918  ordiso2  7096  addlocpr  7598  distrlem1prl  7644  distrlem1pru  7645  ltsopr  7658  addcanprlemu  7677  fzo1fzo0n0  10253  prodfap0  11691  prodfrecap  11692  muldvds2  11963  dvds2add  11971  dvds2sub  11972  dvdstr  11974  qusaddvallemg  12919  mulgnnsubcl  13207  mulgpropdg  13237  ringidss  13528  lmodprop2d  13847  cnpnei  14398  upxp  14451  lgsval4lem  15168
  Copyright terms: Public domain W3C validator