Theorem ianor 984

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 399	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑 ∧ 𝜓))
2		pm4.62 857	. 2 ⊢ ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
3	1, 2	bitr3i 277	1 ⊢ (¬ (𝜑 ∧ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848

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 207  df-an 396  df-or 849

This theorem is referenced by:  anor  985  3ianor  1107  nanor  1495  cadnot  1615  19.33b  1885  neorian  3037  2nreu  4444  tpprceq3  4804  tppreqb  4805  prneimg  4854  prneimg2  4855  prnebg  4856  preq12nebg  4863  opthprneg  4865  opthneg  5486  fr2nr  5662  iresn0n0  6072  xpeq0  6180  difxp  6184  ordtri3or  6416  imadif  6650  ftpg  7176  nf1const  7324  nf1oconst  7325  0mpo0  7516  2mpo0  7682  bropopvvv  8115  bropfvvvv  8117  frxp  8151  soxp  8154  ressuppssdif  8210  mpoxneldm  8237  naddcllem  8714  dfsup2  9484  nelaneq  9639  suc11reg  9659  rankxplim3  9921  kmlem3  10193  cdainflem  10228  isfin5-2  10431  mulge0b  12138  nn0n0n1ge2b  12595  rpneg  13067  mul2lt0bi  13141  xrrebnd  13210  xnn0xaddcl  13277  xmullem2  13307  difreicc  13524  fz0  13579  nelfzo  13704  injresinj  13827  hashunx  14425  swrdnd  14692  swrdnnn0nd  14694  swrdnd0  14695  repswswrd  14822  dfgcd2  16583  ncoprmlnprm  16765  firest  17477  xpcbas  18223  smndex2dnrinv  18928  symgfix2  19434  gsumdixp  20316  0ringnnzr  20525  mplsubrglem  22024  symgmatr01lem  22659  ppttop  23014  fin1aufil  23940  zclmncvs  25182  mbfmax  25684  mdegleb  26103  coemulhi  26293  noetasuplem4  27781  noetainflem4  27785  sltlpss  27945  numedglnl  29161  usgredg2v  29244  clwwlkn  30045  clwwlkneq0  30048  clwwlknon1nloop  30118  trlsegvdeg  30246  1to2vfriswmgr  30298  numclwwlk3lem2  30403  atcvati  32405  difrab2  32517  ofpreima2  32676  hashxpe  32811  fldextrspunlsplem  33723  ordtconnlem1  33923  aean  34245  sitgaddlemb  34350  ballotlemodife  34500  bnj1174  35017  erdszelem10  35205  satfv1  35368  fmla0disjsuc  35403  fmlasucdisj  35404  dfon2lem4  35787  nrmo  36411  poimirlem30  37657  poimirlem31  37658  itg2addnclem  37678  itg2addnclem2  37679  itg2addnclem3  37680  iblabsnclem  37690  ftc1anclem3  37702  areacirclem4  37718  lsatcvat  39051  lkreqN  39171  cvrat  39424  4atlem3  39598  paddasslem17  39838  llnexchb2  39871  dalawlem14  39886  cdleme0nex  40292  lclkrlem2o  41523  lcfrlem19  41563  dvrelog2b  42067  aks4d1p7  42084  aks6d1c2p2  42120  aks6d1c5  42140  sticksstones1  42147  aks6d1c6lem3  42173  ifpnot23  43491  ifpim123g  43513  sqrtcvallem1  43644  ntrneineine1lem  44097  mnringmulrcld  44247  stoweidlem14  46029  stoweidlem26  46041  dfatprc  47142  afvco2  47188  ndmafv2nrn  47234  nfunsnafv2  47237  afv2ndeffv0  47272  nltle2tri  47325  ichnreuop  47459  spr0nelg  47463  evennodd  47630  oddneven  47631  usgrexmpl2trifr  47996  lindslinindsimp1  48374  lindslinindsimp2  48380  line2ylem  48672  line2xlem  48674