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  2082  sbequ8  2153  ralv  2961  reusv5OLD  4725  relop  5015  acsfn0  13877  cmpsub  17455  ballotlemodife  24747  equveliNEW7  29465  sbequ8NEW7  29512  lub0N  29924  glb0N  29928
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