Theorem bi1 117

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Revised by NM, 31-Jan-2015.)

Assertion

Ref	Expression
bi1	⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

Proof of Theorem bi1

Step	Hyp	Ref	Expression
1		df-bi 116	. . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2	1	simpli 110	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
3	2	simpld 111	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  biimpi  119  bicom1  130  biimpd  143  ibd  177  pm5.74  178  bi3ant  223  pm5.501  243  pm5.32d  443  notbi  638  pm5.19  678  con4biddc  825  con1biimdc  841  bijadc  850  pclem6  1335  albi  1427  exbi  1566  equsexd  1690  cbv2h  1707  sbiedh  1743  eumo0  2006  ceqsalt  2683  vtoclgft  2707  spcgft  2734  pm13.183  2792  reu6  2842  reu3  2843  sbciegft  2907  ddifstab  3174  exmidsssnc  4086  fv3  5398  prnmaxl  7244  prnminu  7245  elabgft1  12677  elabgf2  12679  bj-axemptylem  12782  bj-inf2vn  12864  bj-inf2vn2  12865  bj-nn0sucALT  12868