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  1482  exbi  1618  equsexd  1743  cbv2h  1762  cbv2w  1764  sbiedh  1801  eumo0  2076  ceqsalt  2789  vtoclgft  2814  spcgft  2841  pm13.183  2902  reu6  2953  reu3  2954  sbciegft  3020  ddifstab  3296  exmidsssnc  4237  fv3  5584  prnmaxl  7572  prnminu  7573  elabgft1  15508  elabgf2  15510  bj-axemptylem  15622  bj-inf2vn  15704  bj-inf2vn2  15705  bj-nn0sucALT  15708