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 881
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 858 . 2 ((𝜑𝜓) → 𝜑)
61, 5mto 197 1 ¬ (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  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-or 849
This theorem is referenced by:  3pm3.2ni  1490  snsn0non  6509  canthp1lem2  10693  recgt0ii  12174  xrltnr  13161  pnfnlt  13170  nltmnf  13171  smndex1n0mnd  18925  lhop  26055  2lgslem4  27450  nosgnn0  27703  axlowdimlem13  28969  clsk1indlem4  44057  clsk1indlem1  44058  dandysum2p2e4  47010
  Copyright terms: Public domain W3C validator