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 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimpi  120  bicom1  131  biimpd  144  ibd  178  pm5.74  179  bi3ant  224  pm5.501  244  pm5.32d  454  notbi  676  pm5.19  718  con4biddc  869  con1biimdc  885  bijadc  894  pclem6  1423  albi  1521  exbi  1657  equsexd  1782  cbv2h  1801  cbv2w  1803  sbiedh  1840  eumo0  2117  ceqsalt  2848  vtoclgft  2873  spcgft  2902  pm13.183  2964  reu6  3015  reu3  3016  sbciegft  3082  ddifstab  3361  exmidsssnc  4340  fv3  5718  prnmaxl  7855  prnminu  7856  elabgft1  16806  elabgf2  16808  bj-axemptylem  16918  bj-inf2vn  17000  bj-inf2vn2  17001  bj-nn0sucALT  17004