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 878
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 854 . 2 ((𝜑𝜓) → 𝜑)
61, 5mto 200 1 ¬ (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wo 844
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 845
This theorem is referenced by:  snsn0non  6296  canthp1lem2  10067  recgt0ii  11538  xrltnr  12507  pnfnlt  12516  nltmnf  12517  smndex1n0mnd  18073  lhop  24615  2lgslem4  25986  axlowdimlem13  26744  3pm3.2ni  32968  nosgnn0  33190  clsk1indlem4  40603  clsk1indlem1  40604  dandysum2p2e4  43454
  Copyright terms: Public domain W3C validator