Theorem imnan 207

Description: Express implication in terms of conjunction.

Assertion

Ref	Expression
imnan	⊢ ((φ → ¬ ψ) ↔ ¬ (φ ∧ ψ))

Proof of Theorem imnan

Step	Hyp	Ref	Expression
1		df-an 198	. 2 ⊢ ((φ ∧ ψ) ↔ ¬ (φ → ¬ ψ))
2	1	bicon2i 194	1 ⊢ ((φ → ¬ ψ) ↔ ¬ (φ ∧ ψ))

Syntax hints:  ¬ wn 1   → wi 2   ↔ wb 127   ∧ wa 196

This theorem is referenced by:  anass 336  pm5.18 497  dfbi 499  nan 514  ecase2d 558  alinexa 724  eueq3 1430  ssnpss 1573  difin 1670  disj 1733  minel 1743  inssdif0 1754  sotric 2148  dfwe2 2187  ordtri1 2231  ordsucss 2320  onuninsuc 2356  funun 2700  imadif 2714  oalimcl 3162  0nelqs 3234  unblem1 3431  kmlem7 3586  kmlem12 3591  alephnbtwn 3674  aleph1 3676  alephsucdom 3685  cfsuc 3709  genpnnp 3902  nnunb 4520  nneo 4719  sqr2irrlem3 4779  cvnsymt 5722  hatomistic 5755

This theorem was proved from axioms:  ax-1 3¹/SPAN>  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org