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  366  bija  381  albi  1819  spsbbi  2075  cbv2w  2333  cbv2  2401  cbv2h  2404  dfmoeu  2534  2eu6  2656  ax9ALT  2731  ralbi  3102  rexbi  3103  ceqsalt  3471  vtoclgft  3501  spcgft  3536  pm13.183  3607  elabgt  3613  reu6  3671  reu3  3672  sbciegft  3764  axprlem4  5366  fv3  6837  expeq0  13906  t1t0  22597  kqfvima  22979  ufileu  23168  cvmlift2lem1  33504  btwndiff  34420  nn0prpw  34603  bj-animbi  34830  bj-dfbi6  34847  bj-bi3ant  34862  bj-cbv2hv  35070  bj-moeub  35123  bj-ceqsalt0  35159  bj-ceqsalt1  35160  sticksstones3  40354  or3or  41941  bi33imp12  42420  bi23imp1  42425  bi123imp0  42426  eqsbc2VD  42770  imbi12VD  42803  2uasbanhVD  42841  thincciso  46670