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  667  pm5.19  707  con4biddc  858  con1biimdc  874  bijadc  883  pclem6  1385  albi  1479  exbi  1615  equsexd  1740  cbv2h  1759  cbv2w  1761  sbiedh  1798  eumo0  2073  ceqsalt  2786  vtoclgft  2810  spcgft  2837  pm13.183  2898  reu6  2949  reu3  2950  sbciegft  3016  ddifstab  3291  exmidsssnc  4232  fv3  5577  prnmaxl  7548  prnminu  7549  elabgft1  15270  elabgf2  15272  bj-axemptylem  15384  bj-inf2vn  15466  bj-inf2vn2  15467  bj-nn0sucALT  15470