Theorem bi2 121

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 110	. . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2	1	simpli 104	. 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)))
3	2	simprd 107	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑))

Syntax hints:   → wi 4   ∧ wa 97   ↔ wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  bicom1  122  pm5.74  168  bi3ant  213  pm5.32d  423  nbn2  613  pm4.72  736  con4biddc  754  con1biimdc  767  bijadc  776  pclem6  1265  exbir  1325  simplbi2comg  1332  albi  1357  exbi  1495  equsexd  1617  cbv2h  1634  sbiedh  1670  ceqsalt  2580  spcegft  2632  elab3gf  2692  euind  2728  reu6  2730  reuind  2744  sbciegft  2793  iota4  4885  fv3  5197  algcvgblem  9888  bj-notbi  10045  bj-inf2vnlem1  10095