Theorem a1bi 365

Description: Inference introducing a theorem as an antecedent. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)

Hypothesis

Ref	Expression
a1bi.1	⊢ 𝜑

Assertion

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

Proof of Theorem a1bi

Step	Hyp	Ref	Expression
1		a1bi.1	. 2 ⊢ 𝜑
2		biimt 363	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))
3	1, 2	ax-mp 5	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:  mt2bi  366  pm4.83  1021  trut  1539  equsv  2005  equsalv  2263  equsal  2435  2sb6rf  2493  sb4b  2495  sb4bOLD  2496  sbequ8  2539  ralv  3520  relop  5716  acsfn0  16925  cmpsub  22002  ballotlemodife  31750  bj-sbievw1  34164  bj-sbievw  34166  bj-ralvw  34190  wl-equsalvw  34772  wl-equsald  34773  lub0N  36319  glb0N  36323