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

Theorem biimt 362
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 227 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207
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 208
This theorem is referenced by:  pm5.5  363  a1bi  364  mtt  366  abai  824  dedlem0a  1037  ifptru  1067  norasslem2  1524  ceqsralt  3534  reu8  3728  csbiebt  3916  r19.3rz  4445  ralidm  4458  notzfausOLD  5260  reusv2lem5  5299  fncnv  6424  ovmpodxf  7290  brecop  8380  kmlem8  9572  kmlem13  9577  fin71num  9808  ttukeylem6  9925  ltxrlt  10700  rlimresb  14912  acsfn  16920  tgss2  21511  ist1-3  21873  mbflimsup  24182  mdegle0  24586  dchrelbas3  25728  tgcgr4  26231  wl-clabtv  34696  wl-clabt  34697  cdleme32fva  37440  ntrneik2  40307  ntrneix2  40308  ntrneikb  40309  ovmpordxf  44219
  Copyright terms: Public domain W3C validator