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

Theorem 3adant1r 1226
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.)
Hypothesis
Ref Expression
3adant1l.1  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
3adant1r  |-  ( ( ( ph  /\  ta )  /\  ps  /\  ch )  ->  th )

Proof of Theorem 3adant1r
StepHypRef Expression
1 3adant1l.1 . . . 4  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213expb 1199 . . 3  |-  ( (
ph  /\  ( ps  /\ 
ch ) )  ->  th )
32adantlr 474 . 2  |-  ( ( ( ph  /\  ta )  /\  ( ps  /\  ch ) )  ->  th )
433impb 1194 1  |-  ( ( ( ph  /\  ta )  /\  ps  /\  ch )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    /\ w3a 973
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 depends on definitions:  df-bi 116  df-3an 975
This theorem is referenced by:  3adant2r  1228  3adant3r  1230  tfr1onlembacc  6321  tfr1onlembfn  6323  tfr1onlemaccex  6327  tfr1onlemres  6328  tfrcllembfn  6336  tfrcllemaccex  6340  tfrcllemres  6341  tfrcldm  6342  tfrcl  6343  mulassnqg  7346  prarloc  7465  prmuloc  7528  addasssrg  7718  axaddass  7834
  Copyright terms: Public domain W3C validator