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  2301  equsal  2446  2sb6rf  2502  sb4b  2504  sbequ8  2530  ralv  3476  ceqsal  3487  ceqsalv  3489  sbceqal  3800  relop  5830  acsfn0  17748  cmpsub  23625  ballotlemodife  35009  mh-infprim1bi  37165  mh-infprim2bi  37166  bj-equsvt  37504  bj-sbievw1  37588  bj-sbievw  37590  bj-ralvw  37622  wl-2mintru2  38245  wl-equsalvw  38301  wl-equsald  38302  wl-equsaldv  38303  lub0N  40062  glb0N  40066