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  2811  spcgft  2838  pm13.183  2899  reu6  2950  reu3  2951  sbciegft  3017  ddifstab  3292  exmidsssnc  4233  fv3  5578  prnmaxl  7550  prnminu  7551  elabgft1  15340  elabgf2  15342  bj-axemptylem  15454  bj-inf2vn  15536  bj-inf2vn2  15537  bj-nn0sucALT  15540