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  2036  equsalv  2305  equsal  2451  2sb6rf  2507  sb4b  2509  sbequ8  2535  ralv  3483  ceqsal  3494  ceqsalv  3496  sbceqal  3807  relop  5838  acsfn0  17738  cmpsub  23607  ballotlemodife  34953  mh-infprim1bi  37114  mh-infprim2bi  37115  bj-equsvt  37453  bj-sbievw1  37537  bj-sbievw  37539  bj-ralvw  37571  wl-2mintru2  38194  wl-equsalvw  38250  wl-equsald  38251  wl-equsaldv  38252  lub0N  40021  glb0N  40025