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

Theorem biimt 351
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 217 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197
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 198
This theorem is referenced by:  pm5.5  352  a1bi  353  mtt  355  abai  848  dedlem0a  1057  ifptru  1089  ceqsralt  3423  reu8  3600  csbiebt  3748  r19.3rz  4257  ralidm  4270  notzfaus  5032  reusv2lem5  5071  fncnv  6169  ovmpt2dxf  7012  brecop  8071  kmlem8  9260  kmlem13  9265  fin71num  9500  ttukeylem6  9617  ltxrlt  10389  rlimresb  14515  acsfn  16520  tgss2  21001  ist1-3  21363  mbflimsup  23643  mdegle0  24047  dchrelbas3  25173  tgcgr4  25636  cdleme32fva  36212  ntrneik2  38884  ntrneix2  38885  ntrneikb  38886  ovmpt2rdxf  42679
  Copyright terms: Public domain W3C validator