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

Theorem a1bi 327
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 325 . 2  |-  ( ph  ->  ( ps  <->  ( ph  ->  ps ) ) )
31, 2ax-mp 8 1  |-  ( ps  <->  (
ph  ->  ps ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  mt2bi  328  pm4.83  895  truimfal  1335  equveli  1941  sbequ8  2032  ralv  2814  reusv5OLD  4560  relop  4850  acsfn0  13578  cmpsub  17143  ballotlemodife  23072  equveliNEW7  29503  sbequ8NEW7  29550  a12study4  29739  a12lem1  29752  lub0N  30001  glb0N  30005
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 177
  Copyright terms: Public domain W3C validator