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  713  con4biddc  864  con1biimdc  880  bijadc  889  pclem6  1418  albi  1516  exbi  1652  equsexd  1777  cbv2h  1796  cbv2w  1798  sbiedh  1835  eumo0  2110  ceqsalt  2829  vtoclgft  2854  spcgft  2883  pm13.183  2944  reu6  2995  reu3  2996  sbciegft  3062  ddifstab  3339  exmidsssnc  4293  fv3  5662  prnmaxl  7707  prnminu  7708  elabgft1  16374  elabgf2  16376  bj-axemptylem  16487  bj-inf2vn  16569  bj-inf2vn2  16570  bj-nn0sucALT  16573