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  1930  sbequ8  2021  ralv  2803  reusv5OLD  4546  relop  4836  acsfn0  13564  cmpsub  17129  ballotlemodife  23058  a12study4  29190  a12lem1  29203  lub0N  29452  glb0N  29456
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