Theorem a1bi 364

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 362	. 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  365  pm4.83  1038  trut  1566  equsv  2023  equsalv  2302  equsal  2448  2sb6rf  2504  sb4b  2506  sbequ8  2532  ralv  3480  ceqsal  3491  ceqsalv  3493  sbceqal  3805  relop  5822  acsfn0  17692  cmpsub  23457  ballotlemodife  34792  mh-infprim1bi  36903  mh-infprim2bi  36904  bj-equsvt  37243  bj-sbievw1  37327  bj-sbievw  37329  bj-ralvw  37361  wl-2mintru2  37982  wl-equsalvw  38038  wl-equsald  38039  wl-equsaldv  38040  lub0N  39810  glb0N  39814