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

Theorem pm3.2ni 874
Description: Infer negated disjunction of negated premises. (Contributed by NM, 4-Apr-1995.)
Hypotheses
Ref Expression
pm3.2ni.1 ¬ 𝜑
pm3.2ni.2 ¬ 𝜓
Assertion
Ref Expression
pm3.2ni ¬ (𝜑𝜓)

Proof of Theorem pm3.2ni
StepHypRef Expression
1 pm3.2ni.1 . 2 ¬ 𝜑
2 id 22 . . 3 (𝜑𝜑)
3 pm3.2ni.2 . . . 4 ¬ 𝜓
43pm2.21i 119 . . 3 (𝜓𝜑)
52, 4jaoi 851 . 2 ((𝜑𝜓) → 𝜑)
61, 5mto 198 1 ¬ (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 841
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 208  df-or 842
This theorem is referenced by:  snsn0non  6303  canthp1lem2  10064  recgt0ii  11535  xrltnr  12504  pnfnlt  12513  nltmnf  12514  lhop  24542  2lgslem4  25910  axlowdimlem13  26668  3pm3.2ni  32841  nosgnn0  33063  clsk1indlem4  40274  clsk1indlem1  40275  dandysum2p2e4  43115  smndex1n0mnd  43982
  Copyright terms: Public domain W3C validator