Theorem a1bi 361

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 359	. 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 → 𝜓)))
3	1, 2	ax-mp 5	1 ⊢ (𝜓 ↔ (𝜑 → 𝜓))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  mt2bi  362  pm4.83  1022  trut  1539  equsv  1998  equsalv  2253  equsal  2411  2sb6rf  2467  sb4b  2469  sbequ8  2495  ralv  3498  ceqsal  3509  ceqsalv  3511  sbceqal  3844  relop  5857  acsfn0  17647  cmpsub  23324  ballotlemodife  34150  bj-equsvt  36289  bj-sbievw1  36355  bj-sbievw  36357  bj-ralvw  36390  wl-2mintru2  37003  wl-equsalvw  37038  wl-equsald  37039  wl-equsaldv  37040  lub0N  38693  glb0N  38697