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  672  nbn2  705  pm4.72  835  con4biddc  865  con1biimdc  881  bijadc  890  pclem6  1419  exbir  1482  simplbi2comg  1489  albi  1517  exbi  1653  equsexd  1778  cbv2h  1797  cbv2w  1799  sbiedh  1836  ceqsalt  2842  spcegft  2898  elab3gf  2970  euind  3007  reu6  3009  reuind  3025  sbciegft  3076  iota4  5337  fv3  5698  algcvgblem  12771  bj-inf2vnlem1  16866