Theorem biimpr 129

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 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  446  notbi  656  nbn2  687  pm4.72  817  con4biddc  847  con1biimdc  863  bijadc  872  pclem6  1364  exbir  1424  simplbi2comg  1431  albi  1456  exbi  1592  equsexd  1717  cbv2h  1736  cbv2w  1738  sbiedh  1775  ceqsalt  2752  spcegft  2805  elab3gf  2876  euind  2913  reu6  2915  reuind  2931  sbciegft  2981  iota4  5171  fv3  5509  algcvgblem  11981  bj-inf2vnlem1  13852