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  2896  reu8  3047  csbiebt  3203  r19.3rz  3634  r19.3rzv  3636  ralidm  3646  notzfaus  4287  reusv2lem5  4642  reusv7OLD  4649  fncnv  5419  ovmpt2dxf  6099  brecop  6894  kmlem8  7930  kmlem13  7935  fin71num  8170  ttukeylem6  8288  ltxrlt  9040  rlimresb  12246  acsfn  13771  tgss2  16942  ist1-3  17294  mbflimsup  19236  mdegle0  19678  dchrelbas3  20700  wl-pm5.74  25745  wl-dedlem0a  25749  cdleme32fva  30685
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