Theorem ianor 981

Description: Negated conjunction in terms of disjunction (De Morgan's law). Theorem *4.51 of [WhiteheadRussell] p. 120. (Contributed by NM, 14-May-1993.) (Proof shortened by Andrew Salmon, 13-May-2011.)

Assertion

Ref	Expression
ianor	⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))

Proof of Theorem ianor

Step	Hyp	Ref	Expression
1		imnan 401	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
2		pm4.62 855	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
3	1, 2	bitr3i 277	1 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846

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  df-an 398  df-or 847

This theorem is referenced by:  anor  982  3ianor  1108  nanor  1494  cadnot  1617  19.33b  1889  neorian  3038  indifdirOLD  4286  2nreu  4442  tpprceq3  4808  tppreqb  4809  prneimg  4856  prnebg  4857  preq12nebg  4864  opthprneg  4866  opthneg  5482  fr2nr  5655  iresn0n0  6054  xpeq0  6160  difxp  6164  ordtri3or  6397  imadif  6633  ftpg  7154  nf1const  7302  nf1oconst  7303  0mpo0  7492  2mpo0  7655  bropopvvv  8076  bropfvvvv  8078  frxp  8112  soxp  8115  ressuppssdif  8170  mpoxneldm  8197  naddcllem  8675  dfsup2  9439  nelaneq  9594  suc11reg  9614  rankxplim3  9876  kmlem3  10147  cdainflem  10182  isfin5-2  10386  mulge0b  12084  nn0n0n1ge2b  12540  rpneg  13006  mul2lt0bi  13080  xrrebnd  13147  xnn0xaddcl  13214  xmullem2  13244  difreicc  13461  fz0  13516  nelfzo  13637  injresinj  13753  hashunx  14346  swrdnd  14604  swrdnnn0nd  14606  swrdnd0  14607  repswswrd  14734  dfgcd2  16488  ncoprmlnprm  16664  firest  17378  xpcbas  18130  smndex2dnrinv  18796  symgfix2  19284  gsumdixp  20131  0ringnnzr  20302  mplsubrglem  21563  symgmatr01lem  22155  ppttop  22510  fin1aufil  23436  zclmncvs  24665  mbfmax  25166  mdegleb  25582  coemulhi  25768  noetasuplem4  27239  noetainflem4  27243  sltlpss  27401  numedglnl  28404  usgredg2v  28484  clwwlkn  29279  clwwlkneq0  29282  clwwlknon1nloop  29352  trlsegvdeg  29480  1to2vfriswmgr  29532  numclwwlk3lem2  29637  atcvati  31639  difrab2  31738  ofpreima2  31891  hashxpe  32019  ordtconnlem1  32904  aean  33242  sitgaddlemb  33347  ballotlemodife  33496  bnj1174  34014  erdszelem10  34191  satfv1  34354  fmla0disjsuc  34389  fmlasucdisj  34390  dfon2lem4  34758  nrmo  35295  poimirlem30  36518  poimirlem31  36519  itg2addnclem  36539  itg2addnclem2  36540  itg2addnclem3  36541  iblabsnclem  36551  ftc1anclem3  36563  areacirclem4  36579  lsatcvat  37920  lkreqN  38040  cvrat  38293  4atlem3  38467  paddasslem17  38707  llnexchb2  38740  dalawlem14  38755  cdleme0nex  39161  lclkrlem2o  40392  lcfrlem19  40432  dvrelog2b  40931  aks4d1p7  40948  aks6d1c2p2  40957  sticksstones1  40962  ifpnot23  42229  ifpim123g  42251  sqrtcvallem1  42382  ntrneineine1lem  42835  mnringmulrcld  42987  stoweidlem14  44730  stoweidlem26  44742  dfatprc  45838  afvco2  45884  ndmafv2nrn  45930  nfunsnafv2  45933  afv2ndeffv0  45968  nltle2tri  46021  ichnreuop  46140  spr0nelg  46144  evennodd  46311  oddneven  46312  lindslinindsimp1  47138  lindslinindsimp2  47144  line2ylem  47437  line2xlem  47439