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

Theorem biimt 361
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  362  a1bi  363  mtt  365  abai  826  dedlem0a  1043  ifptru  1075  norasslem2  1537  ceqsralt  3477  clel2g  3610  clel4g  3615  reu8  3692  csbiebt  3886  r19.3rz  4455  ralidmOLD  4474  reusv2lem5  5358  fncnv  6575  ovmpodxf  7506  brecop  8750  kmlem8  10094  kmlem13  10099  fin71num  10334  ttukeylem6  10451  ltxrlt  11226  rlimresb  15448  acsfn  17540  tgss2  22340  ist1-3  22703  mbflimsup  25033  mdegle0  25445  dchrelbas3  26589  tgcgr4  27476  wl-clabtv  36052  wl-clabt  36053  cdleme32fva  38903  ntrneik2  42371  ntrneix2  42372  ntrneikb  42373  r19.3rzf  43380  ovmpordxf  46421
  Copyright terms: Public domain W3C validator