Theorem biimp 218

Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.)

Assertion

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

Proof of Theorem biimp

Step	Hyp	Ref	Expression
1		df-bi 210	. . 3 ⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2		simplim 170	. . 3 ⊢ (¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) → ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))))
3	1, 2	ax-mp 5	. 2 ⊢ ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
4		simplim 170	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 → 𝜓))
5	3, 4	syl 17	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210

This theorem is referenced by:  biimpi  219  bicom1  224  biimpd  232  ibd  272  pm5.74  273  pm5.501  370  bija  385  albi  1826  spsbbi  2079  cbv2w  2337  cbv2  2402  cbv2h  2405  dfmoeu  2535  2eu6  2657  ax9ALT  2732  ralbi  3090  ceqsalt  3438  vtoclgft  3468  spcgft  3503  pm13.183  3575  elabgt  3581  reu6  3639  reu3  3640  sbciegft  3732  axprlem4  5319  fv3  6735  expeq0  13665  t1t0  22245  kqfvima  22627  ufileu  22816  cvmlift2lem1  32977  btwndiff  34066  nn0prpw  34249  bj-animbi  34476  bj-dfbi6  34493  bj-bi3ant  34508  bj-cbv2hv  34716  bj-moeub  34770  bj-ceqsalt0  34806  bj-ceqsalt1  34807  sticksstones3  39826  or3or  41308  bi33imp12  41783  bi23imp1  41788  bi123imp0  41789  eqsbc3rVD  42133  imbi12VD  42166  2uasbanhVD  42204  thincciso  46003