MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ianor Structured version   Visualization version   GIF version

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
StepHypRef Expression
1 imnan 401 . 2 ((𝜑 → ¬ 𝜓) ↔ ¬ (𝜑𝜓))
2 pm4.62 855 . 2 ((𝜑 → ¬ 𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
31, 2bitr3i 277 1 (¬ (𝜑𝜓) ↔ (¬ 𝜑 ∨ ¬ 𝜓))
Colors of variables: wff setvar class
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  3040  indifdirOLD  4250  2nreu  4406  tpprceq3  4769  tppreqb  4770  prneimg  4817  prnebg  4818  preq12nebg  4825  opthprneg  4827  opthneg  5443  fr2nr  5616  iresn0n0  6012  xpeq0  6117  difxp  6121  ordtri3or  6354  imadif  6590  ftpg  7107  nf1const  7255  nf1oconst  7256  0mpo0  7445  2mpo0  7607  bropopvvv  8027  bropfvvvv  8029  frxp  8063  soxp  8066  ressuppssdif  8121  mpoxneldm  8148  naddcllem  8627  dfsup2  9387  nelaneq  9542  suc11reg  9562  rankxplim3  9824  kmlem3  10095  cdainflem  10130  isfin5-2  10334  mulge0b  12032  nn0n0n1ge2b  12488  rpneg  12954  mul2lt0bi  13028  xrrebnd  13094  xnn0xaddcl  13161  xmullem2  13191  difreicc  13408  fz0  13463  nelfzo  13584  injresinj  13700  hashunx  14293  swrdnd  14549  swrdnnn0nd  14551  swrdnd0  14552  repswswrd  14679  dfgcd2  16434  ncoprmlnprm  16610  firest  17321  xpcbas  18073  smndex2dnrinv  18732  symgfix2  19205  gsumdixp  20040  0ringnnzr  20755  mplsubrglem  21426  symgmatr01lem  22018  ppttop  22373  fin1aufil  23299  zclmncvs  24528  mbfmax  25029  mdegleb  25445  coemulhi  25631  noetasuplem4  27100  noetainflem4  27104  sltlpss  27258  numedglnl  28137  usgredg2v  28217  clwwlkn  29012  clwwlkneq0  29015  clwwlknon1nloop  29085  trlsegvdeg  29213  1to2vfriswmgr  29265  numclwwlk3lem2  29370  atcvati  31370  difrab2  31468  ofpreima2  31624  hashxpe  31751  ordtconnlem1  32545  aean  32883  sitgaddlemb  32988  ballotlemodife  33137  bnj1174  33655  erdszelem10  33834  satfv1  33997  fmla0disjsuc  34032  fmlasucdisj  34033  dfon2lem4  34400  nrmo  34911  poimirlem30  36137  poimirlem31  36138  itg2addnclem  36158  itg2addnclem2  36159  itg2addnclem3  36160  iblabsnclem  36170  ftc1anclem3  36182  areacirclem4  36198  lsatcvat  37541  lkreqN  37661  cvrat  37914  4atlem3  38088  paddasslem17  38328  llnexchb2  38361  dalawlem14  38376  cdleme0nex  38782  lclkrlem2o  40013  lcfrlem19  40053  dvrelog2b  40552  aks4d1p7  40569  aks6d1c2p2  40578  sticksstones1  40583  ifpnot23  41824  ifpim123g  41846  sqrtcvallem1  41977  ntrneineine1lem  42430  mnringmulrcld  42582  stoweidlem14  44329  stoweidlem26  44341  dfatprc  45436  afvco2  45482  ndmafv2nrn  45528  nfunsnafv2  45531  afv2ndeffv0  45566  nltle2tri  45619  ichnreuop  45738  spr0nelg  45742  evennodd  45909  oddneven  45910  lindslinindsimp1  46612  lindslinindsimp2  46618  line2ylem  46911  line2xlem  46913
  Copyright terms: Public domain W3C validator