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  447  notbi  661  pm5.19  701  con4biddc  852  con1biimdc  868  bijadc  877  pclem6  1369  albi  1461  exbi  1597  equsexd  1722  cbv2h  1741  cbv2w  1743  sbiedh  1780  eumo0  2050  ceqsalt  2756  vtoclgft  2780  spcgft  2807  pm13.183  2868  reu6  2919  reu3  2920  sbciegft  2985  ddifstab  3259  exmidsssnc  4189  fv3  5519  prnmaxl  7450  prnminu  7451  elabgft1  13813  elabgf2  13815  bj-axemptylem  13927  bj-inf2vn  14009  bj-inf2vn2  14010  bj-nn0sucALT  14013