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

Theorem biimt 360
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 42 . 2 (𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 226 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206
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 207
This theorem is referenced by:  pm5.5  361  a1bi  362  mtt  364  abai  827  dedlem0a  1044  ifptru  1075  norasslem2  1535  ceqsralt  3516  clel2g  3659  clel4g  3663  reu8  3739  csbiebt  3928  r19.3rz  4497  reusv2lem5  5402  fncnv  6639  ovmpodxf  7583  brecop  8850  kmlem8  10198  kmlem13  10203  fin71num  10437  ttukeylem6  10554  ltxrlt  11331  rlimresb  15601  acsfn  17702  tgss2  22994  ist1-3  23357  mbflimsup  25701  mdegle0  26116  dchrelbas3  27282  tgcgr4  28539  wl-clabtv  37598  wl-clabt  37599  cdleme32fva  40439  ntrneik2  44105  ntrneix2  44106  ntrneikb  44107  r19.3rzf  45163  ovmpordxf  48255  fulltermc  49143
  Copyright terms: Public domain W3C validator