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

Theorem biimt 335
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 6 . 2  |-  ( ps 
->  ( ph  ->  ps ) )
2 pm2.27 39 . 2  |-  ( ph  ->  ( ( ph  ->  ps )  ->  ps )
)
31, 2impbid2 204 1  |-  ( ph  ->  ( ps  <->  ( ph  ->  ps ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185
This theorem is referenced by:  pm5.5  336  a1bi  337  mtt  339  abai  793  dedlem0a  943  ceqsralt  3094  reu8  3254  csbiebt  3408  r19.3rz  3871  r19.3rzv  3873  ralidm  3883  notzfaus  4567  reusv2lem5  4597  reusv7OLD  4604  fncnv  5582  ovmpt2dxf  6318  brecop  7295  kmlem8  8429  kmlem13  8434  fin71num  8669  ttukeylem6  8786  ltxrlt  9548  rlimresb  13147  acsfn  14701  tgss2  18710  ist1-3  19071  mbflimsup  21262  mdegle0  21666  dchrelbas3  22695  ovmpt2rdxf  30869  cdleme32fva  34389
  Copyright terms: Public domain W3C validator