Theorem bi1 111

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 110	. . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2	1	simpli 104	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
3	2	simpld 105	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

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

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  biimpi  113  bicom1  122  biimpd  132  ibd  167  pm5.74  168  bi3ant  213  pm5.501  233  pm5.32d  423  pm5.19  622  con4biddc  754  con1biimdc  767  bijadc  776  pclem6  1265  albi  1357  exbi  1495  equsexd  1617  cbv2h  1634  sbiedh  1670  eumo0  1931  ceqsalt  2580  vtoclgft  2604  spcgft  2630  pm13.183  2681  reu6  2730  reu3  2731  sbciegft  2793  fv3  5197  prnmaxl  6586  prnminu  6587  elabgft1  9917  elabgf2  9919  bj-axemptylem  10012  bj-notbi  10045  bj-inf2vn  10099  bj-inf2vn2  10100  bj-nn0sucALT  10103