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  843  con1biimdc  859  bijadc  868  pclem6  1356  albi  1448  exbi  1584  equsexd  1709  cbv2h  1728  cbv2w  1730  sbiedh  1767  eumo0  2037  ceqsalt  2738  vtoclgft  2762  spcgft  2789  pm13.183  2850  reu6  2901  reu3  2902  sbciegft  2967  ddifstab  3239  exmidsssnc  4165  fv3  5492  prnmaxl  7409  prnminu  7410  elabgft1  13394  elabgf2  13396  bj-axemptylem  13509  bj-inf2vn  13591  bj-inf2vn2  13592  bj-nn0sucALT  13595