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

Theorem biimt 333
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  334  a1bi  335  mtt  337  abai  793  dedlem0a  950  ifptru  1391  ceqsralt  3071  reu8  3233  csbiebt  3381  r19.3rz  3849  r19.3rzv  3851  ralidm  3862  notzfaus  4553  reusv2lem5  4583  fncnv  5573  ovmpt2dxf  6345  brecop  7340  kmlem8  8468  kmlem13  8473  fin71num  8708  ttukeylem6  8825  ltxrlt  9584  rlimresb  13409  acsfn  15085  tgss2  19593  ist1-3  19955  mbflimsup  22177  mdegle0  22581  dchrelbas3  23649  ovmpt2rdxf  33163  cdleme32fva  36611
  Copyright terms: Public domain W3C validator