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

Theorem biimt 360
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 225 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205
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 206
This theorem is referenced by:  pm5.5  361  a1bi  362  mtt  364  abai  826  dedlem0a  1042  ifptru  1073  norasslem2  1529  ceqsralt  3504  clel2g  3645  clel4g  3650  reu8  3728  csbiebt  3922  r19.3rz  4497  ralidmOLD  4516  reusv2lem5  5402  fncnv  6626  ovmpodxf  7571  brecop  8829  kmlem8  10181  kmlem13  10186  fin71num  10421  ttukeylem6  10538  ltxrlt  11315  rlimresb  15542  acsfn  17639  tgss2  22903  ist1-3  23266  mbflimsup  25608  mdegle0  26026  dchrelbas3  27184  tgcgr4  28348  wl-clabtv  37064  wl-clabt  37065  cdleme32fva  39910  ntrneik2  43522  ntrneix2  43523  ntrneikb  43524  r19.3rzf  44529  ovmpordxf  47402
  Copyright terms: Public domain W3C validator