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

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  pm5.5  362  a1bi  363  mtt  365  abai  832  dedlem0a  1049  ifptru  1080  norasslem2  1542  ceqsralt  3467  clel2g  3604  clel4g  3608  reu8  3681  csbiebt  3867  r19.3rz  4436  reusv2lem5  5338  fncnv  6565  ovmpodxf  7513  brecop  8754  kmlem8  10078  kmlem13  10083  fin71num  10317  ttukeylem6  10434  ltxrlt  11214  rlimresb  15525  acsfn  17623  tgss2  22977  ist1-3  23339  mbflimsup  25658  mdegle0  26067  dchrelbas3  27226  tgcgr4  28624  mh-infprim1bi  36781  wl-clabtv  37964  wl-clabt  37965  cdleme32fva  40936  ntrneik2  44543  ntrneix2  44544  ntrneikb  44545  r19.3rzf  45612  ovmpordxf  48837  fulltermc  50008