Theorem biimp 204

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

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

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 196

This theorem is referenced by:  biimpi  205  bicom1  210  biimpd  218  ibd  257  pm5.74  258  pm5.501  355  bija  369  albi  1736  exbiOLD  1763  cbv2h  2257  mo2v  2465  2eu6  2546  eleq2dOLD  2674  ceqsalt  3201  vtoclgft  3227  vtoclgftOLD  3228  spcgft  3258  pm13.183  3313  reu6  3362  reu3  3363  sbciegft  3433  fv3  6116  expeq0  12752  t1t0  20962  kqfvima  21343  ufileu  21533  cvmlift2lem1  30538  btwndiff  31304  nn0prpw  31488  bj-dfbi6  31730  bj-bi3ant  31747  bj-ssbbi  31811  bj-cbv2hv  31918  bj-eumo0  32018  bj-ceqsalt0  32067  bj-ceqsalt1  32068  bj-ax9  32083  or3or  37339  bi33imp12  37717  bi23imp1  37722  bi123imp0  37723  eqsbc3rVD  38097  imbi12VD  38131  2uasbanhVD  38169