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  2069  ceqsalt  2778  vtoclgft  2802  spcgft  2829  pm13.183  2890  reu6  2941  reu3  2942  sbciegft  3008  ddifstab  3282  exmidsssnc  4221  fv3  5557  prnmaxl  7516  prnminu  7517  elabgft1  14983  elabgf2  14985  bj-axemptylem  15097  bj-inf2vn  15179  bj-inf2vn2  15180  bj-nn0sucALT  15183