MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biimt 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

Proof of Theorem biimt
StepHypRef Expression
1 ax-1 6 . 2
2 pm2.27 39 . 2
31, 2impbid2 204 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184
This theorem is referenced by:  pm5.5  336  a1bi  337  mtt  339  abai  795  dedlem0a  952  ceqsralt  3133  reu8  3295  csbiebt  3454  r19.3rz  3920  r19.3rzv  3922  ralidm  3933  notzfaus  4627  reusv2lem5  4657  reusv7OLD  4664  fncnv  5657  ovmpt2dxf  6428  brecop  7423  kmlem8  8558  kmlem13  8563  fin71num  8798  ttukeylem6  8915  ltxrlt  9676  rlimresb  13388  acsfn  15056  tgss2  19489  ist1-3  19850  mbflimsup  22073  mdegle0  22477  dchrelbas3  23513  ovmpt2rdxf  32928  cdleme32fva  36163
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
  Copyright terms: Public domain W3C validator