Theorem biimpr 130

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

Assertion

Ref	Expression
biimpr	⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

Proof of Theorem biimpr

Step	Hyp	Ref	Expression
1		df-bi 117	. . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2	1	simpli 111	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
3	2	simprd 114	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

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

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bicom1  131  pm5.74  179  bi3ant  224  pm5.32d  450  notbi  668  nbn2  699  pm4.72  829  con4biddc  859  con1biimdc  875  bijadc  884  pclem6  1394  exbir  1456  simplbi2comg  1463  albi  1491  exbi  1627  equsexd  1752  cbv2h  1771  cbv2w  1773  sbiedh  1810  ceqsalt  2798  spcegft  2852  elab3gf  2923  euind  2960  reu6  2962  reuind  2978  sbciegft  3029  iota4  5252  fv3  5601  algcvgblem  12404  bj-inf2vnlem1  15943