Theorem bi2 129

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

Assertion

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

Proof of Theorem bi2

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-1 5  ax-2 6  ax-mp 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  441  nbn2  654  pm4.72  778  con4biddc  798  con1biimdc  811  bijadc  820  pclem6  1320  exbir  1380  simplbi2comg  1387  albi  1412  exbi  1551  equsexd  1675  cbv2h  1692  sbiedh  1728  ceqsalt  2667  spcegft  2720  elab3gf  2787  euind  2824  reu6  2826  reuind  2842  sbciegft  2891  iota4  5042  fv3  5376  algcvgblem  11523  bj-notbi  12704  bj-inf2vnlem1  12753