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  2302  equsal  2447  2sb6rf  2503  sb4b  2505  sbequ8  2531  ralv  3477  ceqsal  3488  ceqsalv  3490  sbceqal  3800  relop  5828  acsfn0  17827  cmpsub  23711  ballotlemodife  35123  mh-infprim1bi  37314  mh-infprim2bi  37315  bj-equsvt  37653  bj-sbievw1  37737  bj-sbievw  37739  bj-ralvw  37771  wl-2mintru2  38394  wl-equsalvw  38450  wl-equsald  38451  wl-equsaldv  38452  lub0N  40226  glb0N  40230