Theorem imnan 242

Description: Express implication in terms of conjunction.

Assertion

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

Proof of Theorem imnan

Step	Hyp	Ref	Expression
1		df-an 225	. 2 ⊢ ((φ ⋀ ψ) ↔ ¬ (φ → ¬ ψ))
2	1	con2bii 221	1 ⊢ ((φ → ¬ ψ) ↔ ¬ (φ ⋀ ψ))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223

This theorem is referenced by:  pm4.15 353  anass 439  pm5.18 659  pm5.17 667  dfbi 669  nan 688  ecase2d 750  nicodraw 950  alinexa 1040  dfsb3 1224  a12lem2 1375  a12study 1376  ralinexa 1680  eueq3 1915  ssnpss 2145  difin 2241  disj 2307  minel 2320  inssdif0 2329  sotric 2855  fr0 2922  dfwe2 2930  ordtri1 2975  ordsucss 3064  onuninsuc 3103  ordunisuc2 3110  funun 3546  imadif 3566  oalimcl 4184  omlimcl 4199  0nelqs 4288  unblem1 4523  suppr 4570  kmlem4 4748  alephnbtwn 4848  alephsucpw 4850  alephsucdom 4860  cfsuc 4895  genpnnp 5088  ltnsym2t 5514  xrltnsym2t 5532  nneo 6152  sqr2irrlem3 6664  aleph1re 7502  clsval2 7635  ntreq0 7658  bcthlem7 7955  nmounbi 8384  pilem1 8609  cvnsymt 10155  hatomistic 10226  cnfilca 10487

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

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain