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 ⊢ (𝜓 ↔ (𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  mt2bi  366  pm4.83  1042  trut  1576  equsv  2038  equsalv  2305  equsal  2449  2sb6rf  2505  sb4b  2507  sbequ8  2533  ralv  3480  ceqsal  3491  ceqsalv  3493  sbceqal  3803  relop  5838  acsfn0  17884  cmpsub  23773  ballotlemodife  35241  mh-infprim1bi  37549  mh-infprim2bi  37550  bj-equsvt  37888  bj-sbievw1  37972  bj-sbievw  37974  bj-ralvw  38006  wl-2mintru2  38682  wl-equsalvw  38738  wl-equsald  38739  wl-equsaldv  38740  lub0N  40512  glb0N  40516