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

Step	Hyp	Ref	Expression
1		ax-1 6	. 2
2		pm2.27 39	. 2
3	1, 2	impbid2 204	1

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