MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a1bi 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  1351  equsalhw  1850  equsal  1954  equveli  2023  sbequ8  2112  ralv  2912  reusv5OLD  4673  relop  4963  acsfn0  13812  cmpsub  17385  ballotlemodife  24534  equveliNEW7  28864  sbequ8NEW7  28911  lub0N  29304  glb0N  29308
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