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  672  pm5.19  714  con4biddc  865  con1biimdc  881  bijadc  890  pclem6  1419  albi  1517  exbi  1653  equsexd  1778  cbv2h  1797  cbv2w  1799  sbiedh  1836  eumo0  2113  ceqsalt  2842  vtoclgft  2867  spcgft  2896  pm13.183  2958  reu6  3009  reu3  3010  sbciegft  3076  ddifstab  3355  exmidsssnc  4321  fv3  5698  prnmaxl  7819  prnminu  7820  elabgft1  16676  elabgf2  16678  bj-axemptylem  16788  bj-inf2vn  16870  bj-inf2vn2  16871  bj-nn0sucALT  16874