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  438  nbn2  646  pm4.72  770  con4biddc  788  con1biimdc  801  bijadc  810  pclem6  1306  exbir  1366  simplbi2comg  1373  albi  1398  exbi  1536  equsexd  1658  cbv2h  1675  sbiedh  1711  ceqsalt  2626  spcegft  2678  elab3gf  2744  euind  2780  reu6  2782  reuind  2796  sbciegft  2845  iota4  4915  fv3  5229  algcvgblem  10575  bj-notbi  10874  bj-inf2vnlem1  10923