Theorem bi2 121

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.)

Assertion

Ref	Expression
bi2	⊢ ((φ ↔ ψ) → (ψ → φ))

Proof of Theorem bi2

Step	Hyp	Ref	Expression
1		df-bi 110	. . 3 ⊢ (((φ ↔ ψ) → ((φ → ψ) ∧ (ψ → φ))) ∧ (((φ → ψ) ∧ (ψ → φ)) → (φ ↔ ψ)))
2	1	simpli 104	. 2 ⊢ ((φ ↔ ψ) → ((φ → ψ) ∧ (ψ → φ)))
3	2	simprd 107	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  ax-ia2 100

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bicom1  122  pm5.74  168  bi3ant  213  pm5.32d  423  nbn2  612  pm4.72  735  con4biddc  753  con1biimdc  766  bijadc  775  pclem6  1264  exbir  1322  simplbi2comg  1329  albi  1354  exbi  1492  equsexd  1614  cbv2h  1631  sbiedh  1667  ceqsalt  2574  spcegft  2626  elab3gf  2686  euind  2722  reu6  2724  reuind  2738  sbciegft  2787  iota4  4828  fv3  5140  bj-notbi  9380  bj-inf2vnlem1  9430