Users' Mathboxes Mathbox for Jeff Hankins < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  a1i4 Unicode version

Theorem a1i4 26304
Description: Add an antecedent to a wff. (Contributed by Jeff Hankins, 4-Aug-2009.)
Hypothesis
Ref Expression
a1i4.1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )
Assertion
Ref Expression
a1i4  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )

Proof of Theorem a1i4
StepHypRef Expression
1 a1i4.1 . 2  |-  ( ph  ->  ( ps  ->  ( ch  ->  ta ) ) )
2 ax-1 5 . 2  |-  ( ta 
->  ( th  ->  ta ) )
31, 2syl8 65 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  ad4ant123  28521  ad5ant12  28527  ad5ant13  28528  ad5ant14  28529  ad5ant15  28530  ad5ant23  28531  ad5ant24  28532  ad5ant25  28533  ad5ant245  28534  ad5ant234  28535  ad5ant235  28536  ad5ant123  28537  ad5ant124  28538  ad5ant125  28539  ad5ant134  28540  ad5ant135  28541  ad5ant145  28542
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator