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  667  nbn2  698  pm4.72  828  con4biddc  858  con1biimdc  874  bijadc  883  pclem6  1385  exbir  1447  simplbi2comg  1454  albi  1479  exbi  1615  equsexd  1740  cbv2h  1759  cbv2w  1761  sbiedh  1798  ceqsalt  2786  spcegft  2840  elab3gf  2911  euind  2948  reu6  2950  reuind  2966  sbciegft  3017  iota4  5235  fv3  5578  algcvgblem  12190  bj-inf2vnlem1  15532