MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a1ddd Structured version   Visualization version   Unicode version

Theorem a1ddd 76
Description: Triple deduction introducing an antecedent to a wff. Deduction associated with a1dd 47. Double deduction associated with a1d 26. Triple deduction associated with ax-1 6 and a1i 11. (Contributed by Jeff Hankins, 4-Aug-2009.)
Hypothesis
Ref Expression
a1ddd.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )
Assertion
Ref Expression
a1ddd  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem a1ddd
StepHypRef Expression
1 a1ddd.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )
2 ax-1 6 . 2  |-  ( ta 
->  ( th  ->  ta ) )
31, 2syl8 72 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  ad4ant123  1244  ad5ant13  1251  ad5ant14  1252  ad5ant15  1253  ad5ant23  1254  ad5ant24  1255  ad5ant25  1256  ad5ant245  1257  ad5ant234  1258  ad5ant235  1259  ad5ant123  1260  ad5ant124  1261  ad5ant125  1262  ad5ant134  1263  ad5ant135  1264  ad5ant145  1265
  Copyright terms: Public domain W3C validator