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

Theorem biimt 349
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 216 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196
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 197
This theorem is referenced by:  pm5.5  350  a1bi  351  mtt  353  abai  871  dedlem0a  1030  ifptru  1061  ceqsralt  3370  reu8  3544  csbiebt  3695  r19.3rz  4207  ralidm  4220  notzfaus  4990  reusv2lem5  5023  fncnv  6124  ovmpt2dxf  6953  brecop  8010  kmlem8  9192  kmlem13  9197  fin71num  9432  ttukeylem6  9549  ltxrlt  10321  rlimresb  14516  acsfn  16542  tgss2  21014  ist1-3  21376  mbflimsup  23653  mdegle0  24057  dchrelbas3  25184  tgcgr4  25647  cdleme32fva  36246  ntrneik2  38911  ntrneix2  38912  ntrneikb  38913  ovmpt2rdxf  42646
  Copyright terms: Public domain W3C validator