Theorem biimp 214

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 206	. . 3 ⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓)))
2		simplim 167	. . 3 ⊢ (¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) → ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))))
3	1, 2	ax-mp 5	. 2 ⊢ ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))
4		simplim 167	. 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 → 𝜓))
5	3, 4	syl 17	1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓))

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

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 206

This theorem is referenced by:  biimpi  215  bicom1  220  biimpd  228  ibd  268  pm5.74  269  pm5.501  365  bija  379  albi  1818  spsbbi  2074  cbv2w  2331  cbv2  2400  cbv2h  2403  dfmoeu  2528  2eu6  2650  ax9ALT  2725  ralbi  3101  rexbi  3102  raleleq  3335  ceqsalt  3504  vtoclgft  3539  spcgft  3579  pm13.183  3657  elabgt  3663  reu6  3723  reu3  3724  sbciegft  3816  axprlem4  5425  fv3  6910  expeq0  14064  t1t0  23074  kqfvima  23456  ufileu  23645  cvmlift2lem1  34589  btwndiff  35301  nn0prpw  35513  bj-animbi  35740  bj-dfbi6  35757  bj-bi3ant  35772  bj-cbv2hv  35980  bj-moeub  36033  bj-ceqsalt0  36069  bj-ceqsalt1  36070  sticksstones3  41272  or3or  43078  bi33imp12  43555  bi23imp1  43560  bi123imp0  43561  eqsbc2VD  43905  imbi12VD  43938  2uasbanhVD  43976  nimnbi  44161  thincciso  47758