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

Theorem a1i4 26299
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 67 1  |-  ( ph  ->  ( ps  ->  ( ch  ->  ( th  ->  ta ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  ad4ant123  28540  ad5ant13  28547  ad5ant14  28548  ad5ant15  28549  ad5ant23  28550  ad5ant24  28551  ad5ant25  28552  ad5ant245  28553  ad5ant234  28554  ad5ant235  28555  ad5ant123  28556  ad5ant124  28557  ad5ant125  28558  ad5ant134  28559  ad5ant135  28560  ad5ant145  28561
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator