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

Theorem biimt 327
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 38 . 2  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)
31, 2impbid2 197 1  |-  ( ph  ->  ( ps  <->  ( ph  ->  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178
This theorem is referenced by:  pm5.5  328  a1bi  329  mtt  331  abai  772  dedlem0a  920  ceqsralt  2980  reu8  3131  csbiebt  3288  r19.3rz  3720  r19.3rzv  3722  ralidm  3732  notzfaus  4375  reusv2lem5  4729  reusv7OLD  4736  fncnv  5516  ovmpt2dxf  6200  brecop  6998  kmlem8  8038  kmlem13  8043  fin71num  8278  ttukeylem6  8395  ltxrlt  9147  rlimresb  12360  acsfn  13885  tgss2  17053  ist1-3  17414  mbflimsup  19559  mdegle0  20001  dchrelbas3  21023  wl-pm5.74  26229  wl-dedlem0a  26233  cdleme32fva  31235
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 179
  Copyright terms: Public domain W3C validator