Theorem bi2 129

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 116	. . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2	1	simpli 110	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
3	2	simprd 113	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

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

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bicom1  130  pm5.74  178  bi3ant  223  pm5.32d  445  notbi  655  nbn2  686  pm4.72  812  con4biddc  842  con1biimdc  858  bijadc  867  pclem6  1352  exbir  1412  simplbi2comg  1419  albi  1444  exbi  1583  equsexd  1707  cbv2h  1724  sbiedh  1760  ceqsalt  2707  spcegft  2760  elab3gf  2829  euind  2866  reu6  2868  reuind  2884  sbciegft  2934  iota4  5101  fv3  5437  algcvgblem  11719  bj-inf2vnlem1  13157