Theorem biimp 118

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 117	. . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2	1	simpli 111	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
3	2	simpld 112	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimpi  120  bicom1  131  biimpd  144  ibd  178  pm5.74  179  bi3ant  224  pm5.501  244  pm5.32d  450  notbi  670  pm5.19  711  con4biddc  862  con1biimdc  878  bijadc  887  pclem6  1416  albi  1514  exbi  1650  equsexd  1775  cbv2h  1794  cbv2w  1796  sbiedh  1833  eumo0  2108  ceqsalt  2826  vtoclgft  2851  spcgft  2880  pm13.183  2941  reu6  2992  reu3  2993  sbciegft  3059  ddifstab  3336  exmidsssnc  4286  fv3  5649  prnmaxl  7671  prnminu  7672  elabgft1  16100  elabgf2  16102  bj-axemptylem  16213  bj-inf2vn  16295  bj-inf2vn2  16296  bj-nn0sucALT  16299