Theorem bi1 117

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Revised by NM, 31-Jan-2015.)

Assertion

Ref	Expression
bi1	⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

Proof of Theorem bi1

Step	Hyp	Ref	Expression
1		df-bi 116	. . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2	1	simpli 110	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
3	2	simpld 111	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpi  119  bicom1  130  biimpd  143  ibd  177  pm5.74  178  bi3ant  223  pm5.501  243  pm5.32d  445  notbi  655  pm5.19  695  con4biddc  842  con1biimdc  858  bijadc  867  pclem6  1352  albi  1444  exbi  1583  equsexd  1707  cbv2h  1724  sbiedh  1760  eumo0  2028  ceqsalt  2707  vtoclgft  2731  spcgft  2758  pm13.183  2817  reu6  2868  reu3  2869  sbciegft  2934  ddifstab  3203  exmidsssnc  4121  fv3  5437  prnmaxl  7289  prnminu  7290  elabgft1  12974  elabgf2  12976  bj-axemptylem  13079  bj-inf2vn  13161  bj-inf2vn2  13162  bj-nn0sucALT  13165