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

Theorem biimt 350
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  351  a1bi  352  mtt  354  abai  835  dedlem0a  999  ifptru  1022  ceqsralt  3219  reu8  3389  csbiebt  3539  r19.3rz  4040  ralidm  4053  notzfaus  4810  reusv2lem5  4843  fncnv  5930  ovmpt2dxf  6751  brecop  7800  kmlem8  8939  kmlem13  8944  fin71num  9179  ttukeylem6  9296  ltxrlt  10068  rlimresb  14246  acsfn  16260  tgss2  20731  ist1-3  21093  mbflimsup  23373  mdegle0  23775  dchrelbas3  24897  tgcgr4  25360  cdleme32fva  35244  ntrneik2  37911  ntrneix2  37912  ntrneikb  37913  ovmpt2rdxf  41435
  Copyright terms: Public domain W3C validator