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

Theorem biimt 325
Description: A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996.)
Assertion
Ref Expression
biimt  |-  ( ph  ->  ( ps  <->  ( ph  ->  ps ) ) )

Proof of Theorem biimt
StepHypRef Expression
1 ax-1 5 . 2  |-  ( ps 
->  ( ph  ->  ps ) )
2 pm2.27 35 . 2  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)
31, 2impbid2 195 1  |-  ( ph  ->  ( ps  <->  ( ph  ->  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176
This theorem is referenced by:  pm5.5  326  a1bi  327  mtt  329  abai  770  dedlem0a  918  ceqsralt  2811  reu8  2961  csbiebt  3117  r19.3rz  3545  r19.3rzv  3547  ralidm  3557  notzfaus  4185  reusv2lem5  4539  reusv7OLD  4546  fncnv  5314  ovmpt2dxf  5973  brecop  6751  kmlem8  7783  kmlem13  7788  fin71num  8023  ttukeylem6  8141  ltxrlt  8893  rlimresb  12039  acsfn  13561  tgss2  16725  ist1-3  17077  mbflimsup  19021  mdegle0  19463  dchrelbas3  20477  wl-pm5.74  24918  wl-dedlem0a  24922  cdleme32fva  30626
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