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

Theorem 3ad2antl1 1159
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 1154 1  |-  ( ( ( ph  /\  ps  /\ 
ta )  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104    /\ w3a 978
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 980
This theorem is referenced by:  acexmid  5873  ordiso2  7033  addlocpr  7534  distrlem1prl  7580  distrlem1pru  7581  ltsopr  7594  addcanprlemu  7613  fzo1fzo0n0  10180  prodfap0  11548  prodfrecap  11549  muldvds2  11819  dvds2add  11827  dvds2sub  11828  dvdstr  11830  qusaddvallemg  12746  mulgnnsubcl  12989  mulgpropdg  13018  ringidss  13205  cnpnei  13650  upxp  13703  lgsval4lem  14343
  Copyright terms: Public domain W3C validator