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 857 . 2 ((𝜑𝜓) → 𝜑)
61, 5mto 200 1 ¬ (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 847
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 210  df-or 848
This theorem is referenced by:  snsn0non  6337  canthp1lem2  10272  recgt0ii  11743  xrltnr  12716  pnfnlt  12725  nltmnf  12726  smndex1n0mnd  18344  lhop  24918  2lgslem4  26292  axlowdimlem13  27050  3pm3.2ni  33376  nosgnn0  33603  clsk1indlem4  41339  clsk1indlem1  41340  dandysum2p2e4  44173
  Copyright terms: Public domain W3C validator