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  1530  ceqsralt  3531  reu8  3727  csbiebt  3915  r19.3rz  4445  ralidm  4458  notzfausOLD  5266  reusv2lem5  5306  fncnv  6430  ovmpodxf  7303  brecop  8393  kmlem8  9586  kmlem13  9591  fin71num  9822  ttukeylem6  9939  ltxrlt  10714  rlimresb  14925  acsfn  16933  tgss2  21598  ist1-3  21960  mbflimsup  24270  mdegle0  24674  dchrelbas3  25817  tgcgr4  26320  wl-clabtv  34833  wl-clabt  34834  cdleme32fva  37577  ntrneik2  40448  ntrneix2  40449  ntrneikb  40450  ovmpordxf  44394