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

Theorem biimt 326
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 37 . 2  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)
31, 2impbid2 196 1  |-  ( ph  ->  ( ps  <->  ( ph  ->  ps ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177
This theorem is referenced by:  pm5.5  327  a1bi  328  mtt  330  abai  771  dedlem0a  919  ceqsralt  2939  reu8  3090  csbiebt  3247  r19.3rz  3679  r19.3rzv  3681  ralidm  3691  notzfaus  4334  reusv2lem5  4687  reusv7OLD  4694  fncnv  5474  ovmpt2dxf  6158  brecop  6956  kmlem8  7993  kmlem13  7998  fin71num  8233  ttukeylem6  8350  ltxrlt  9102  rlimresb  12314  acsfn  13839  tgss2  17007  ist1-3  17367  mbflimsup  19511  mdegle0  19953  dchrelbas3  20975  wl-pm5.74  26132  wl-dedlem0a  26136  cdleme32fva  30919
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 178
  Copyright terms: Public domain W3C validator