Theorem biimt 363

Description: A wff is equivalent to itself with true antecedent. (Contributed by NM, 28-Jan-1996.)

Assertion

Ref	Expression
biimt	⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))

Proof of Theorem biimt

Step	Hyp	Ref	Expression
1		ax-1 6	. 2 ⊢ (𝜓 → (𝜑 → 𝜓))
2		pm2.27 42	. 2 ⊢ (𝜑 → ((𝜑 → 𝜓) → 𝜓))
3	1, 2	impbid2 228	1 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  pm5.5  364  a1bi  365  mtt  367  abai  824  dedlem0a  1038  ifptru  1068  norasslem2  1525  ceqsralt  3527  reu8  3722  csbiebt  3910  r19.3rz  4440  ralidm  4453  notzfausOLD  5254  reusv2lem5  5293  fncnv  6420  ovmpodxf  7292  brecop  8382  kmlem8  9575  kmlem13  9580  fin71num  9811  ttukeylem6  9928  ltxrlt  10703  rlimresb  14914  acsfn  16922  tgss2  21587  ist1-3  21949  mbflimsup  24259  mdegle0  24663  dchrelbas3  25806  tgcgr4  26309  wl-clabtv  34821  wl-clabt  34822  cdleme32fva  37565  ntrneik2  40432  ntrneix2  40433  ntrneikb  40434  ovmpordxf  44377