Theorem bi2 128

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 115	. . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2	1	simpli 109	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
3	2	simprd 112	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  bicom1  129  pm5.74  177  bi3ant  222  pm5.32d  437  nbn2  645  pm4.72  769  con4biddc  787  con1biimdc  800  bijadc  809  pclem6  1305  exbir  1365  simplbi2comg  1372  albi  1397  exbi  1535  equsexd  1657  cbv2h  1674  sbiedh  1710  ceqsalt  2625  spcegft  2677  elab3gf  2743  euind  2779  reu6  2781  reuind  2795  sbciegft  2844  iota4  4905  fv3  5218  algcvgblem  10431  bj-notbi  10716  bj-inf2vnlem1  10765