Theorem biimp 117

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

Assertion

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

Proof of Theorem biimp

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  446  notbi  656  pm5.19  696  con4biddc  847  con1biimdc  863  bijadc  872  pclem6  1364  albi  1456  exbi  1592  equsexd  1717  cbv2h  1736  cbv2w  1738  sbiedh  1775  eumo0  2045  ceqsalt  2752  vtoclgft  2776  spcgft  2803  pm13.183  2864  reu6  2915  reu3  2916  sbciegft  2981  ddifstab  3254  exmidsssnc  4182  fv3  5509  prnmaxl  7429  prnminu  7430  elabgft1  13659  elabgf2  13661  bj-axemptylem  13774  bj-inf2vn  13856  bj-inf2vn2  13857  bj-nn0sucALT  13860