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  621  con4biddc  753  con1biimdc  766  bijadc  775  pclem6  1264  albi  1354  exbi  1492  equsexd  1614  cbv2h  1631  sbiedh  1667  eumo0  1928  ceqsalt  2574  vtoclgft  2598  spcgft  2624  pm13.183  2675  reu6  2724  reu3  2725  sbciegft  2787  fv3  5140  prnmaxl  6471  prnminu  6472  elabgft1  9252  elabgf2  9254  bj-axemptylem  9347  bj-notbi  9380  bj-inf2vn  9434  bj-inf2vn2  9435  bj-nn0sucALT  9438