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 41 . 2 (𝜑 → ((𝜑𝜓) → 𝜓))
31, 2impbid2 215 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 195
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 196
This theorem is referenced by:  pm5.5  350  a1bi  351  mtt  353  abai  832  dedlem0a  991  ifptru  1017  ceqsralt  3202  reu8  3369  csbiebt  3519  r19.3rz  4014  ralidm  4027  notzfaus  4766  reusv2lem5  4799  fncnv  5876  ovmpt2dxf  6684  brecop  7727  kmlem8  8862  kmlem13  8867  fin71num  9102  ttukeylem6  9219  ltxrlt  9987  rlimresb  14144  acsfn  16143  tgss2  20602  ist1-3  20963  mbflimsup  23239  mdegle0  23641  dchrelbas3  24763  tgcgr4  25226  cdleme32fva  34743  ntrneik2  37410  ntrneix2  37411  ntrneikb  37412  ovmpt2rdxf  41910
  Copyright terms: Public domain W3C validator