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

Theorem 3adant3r 1167
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
3adant3r  |-  ( (
ph  /\  ps  /\  ( ch  /\  ta ) )  ->  th )

Proof of Theorem 3adant3r
StepHypRef Expression
1 3adant1l.1 . . . 4  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
213com13 1144 . . 3  |-  ( ( ch  /\  ps  /\  ph )  ->  th )
323adant1r 1163 . 2  |-  ( ( ( ch  /\  ta )  /\  ps  /\  ph )  ->  th )
433com13 1144 1  |-  ( (
ph  /\  ps  /\  ( ch  /\  ta ) )  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    /\ w3a 920
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 922
This theorem is referenced by:  addassnqg  6634  mulassnqg  6636  prarloc  6755  ltpopr  6847  ltexprlemfl  6861  ltexprlemfu  6863  addasssrg  6995  axaddass  7100  apmul1  7943  ltmul2  8001  lemul2  8002  dvdscmulr  10369  dvdsmulcr  10370  modremain  10473  ndvdsadd  10475  rpexp12i  10678
  Copyright terms: Public domain W3C validator