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  1575  equsv  2035  equsalv  2301  equsal  2446  2sb6rf  2502  sb4b  2504  sbequ8  2530  ralv  3476  ceqsal  3487  ceqsalv  3489  sbceqal  3799  relop  5829  acsfn0  17843  cmpsub  23727  ballotlemodife  35180  mh-infprim1bi  37430  mh-infprim2bi  37431  bj-equsvt  37769  bj-sbievw1  37853  bj-sbievw  37855  bj-ralvw  37887  wl-2mintru2  38523  wl-equsalvw  38579  wl-equsald  38580  wl-equsaldv  38581  lub0N  40355  glb0N  40359