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  447  notbi  661  nbn2  692  pm4.72  822  con4biddc  852  con1biimdc  868  bijadc  877  pclem6  1369  exbir  1429  simplbi2comg  1436  albi  1461  exbi  1597  equsexd  1722  cbv2h  1741  cbv2w  1743  sbiedh  1780  ceqsalt  2756  spcegft  2809  elab3gf  2880  euind  2917  reu6  2919  reuind  2935  sbciegft  2985  iota4  5178  fv3  5519  algcvgblem  12003  bj-inf2vnlem1  14005