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 880
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 197 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 207  df-or 848
This theorem is referenced by:  3pm3.2ni  1487  snsn0non  6511  canthp1lem2  10691  recgt0ii  12172  xrltnr  13159  pnfnlt  13168  nltmnf  13169  smndex1n0mnd  18938  lhop  26070  2lgslem4  27465  nosgnn0  27718  axlowdimlem13  28984  clsk1indlem4  44034  clsk1indlem1  44035  dandysum2p2e4  46948
  Copyright terms: Public domain W3C validator