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

Theorem a1bi 328
Description: Inference rule introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)
Hypothesis
Ref Expression
a1bi.1  |-  ph
Assertion
Ref Expression
a1bi  |-  ( ps  <->  (
ph  ->  ps ) )

Proof of Theorem a1bi
StepHypRef Expression
1 a1bi.1 . 2  |-  ph
2 biimt 326 . 2  |-  ( ph  ->  ( ps  <->  ( ph  ->  ps ) ) )
31, 2ax-mp 8 1  |-  ( ps  <->  (
ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  mt2bi  329  pm4.83  896  truimfal  1354  equsalhw  1860  equsal  1999  equveliOLD  2086  sbequ8  2148  ralv  2969  reusv5OLD  4733  relop  5023  acsfn0  13885  cmpsub  17463  ballotlemodife  24755  equveliNEW7  29528  sbequ8NEW7  29575  lub0N  29987  glb0N  29991
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 178
  Copyright terms: Public domain W3C validator