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

Theorem biimt 365
 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 229 1 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209 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 210 This theorem is referenced by:  pm5.5  366  a1bi  367  mtt  369  abai  826  dedlem0a  1040  ifptru  1072  norasslem2  1533  ceqsralt  3445  clel2g  3571  clel4g  3576  reu8  3648  csbiebt  3835  r19.3rz  4391  ralidmOLD  4409  notzfausOLD  5232  reusv2lem5  5272  fncnv  6409  ovmpodxf  7296  brecop  8401  kmlem8  9610  kmlem13  9615  fin71num  9850  ttukeylem6  9967  ltxrlt  10742  rlimresb  14963  acsfn  16981  tgss2  21680  ist1-3  22042  mbflimsup  24359  mdegle0  24770  dchrelbas3  25914  tgcgr4  26417  wl-clabtv  35267  wl-clabt  35268  cdleme32fva  38006  ntrneik2  41161  ntrneix2  41162  ntrneikb  41163  ovmpordxf  45100
 Copyright terms: Public domain W3C validator