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

Theorem nsyl5 159
Description: A negated syllogism inference. (Contributed by Wolf Lammen, 20-May-2024.)
Hypotheses
Ref Expression
nsyl4.1 (𝜑𝜓)
nsyl4.2 𝜑𝜒)
Assertion
Ref Expression
nsyl5 𝜓𝜒)

Proof of Theorem nsyl5
StepHypRef Expression
1 nsyl4.1 . . 3 (𝜑𝜓)
2 nsyl4.2 . . 3 𝜑𝜒)
31, 2nsyl4 158 . 2 𝜒𝜓)
43con1i 147 1 𝜓𝜒)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem is referenced by:  pm5.55  947  euor2  2609  moanimlem  2614  moexexlem  2622  eueq3  3706  opprc1  4896  opprc2  4897  mosubopt  5509  nfvres  6929  fvco4i  6989  fvmptex  7009  fvopab4ndm  7024  ressnop0  7147  csbriota  7377  ovprc  7443  ovprc1  7444  ovprc2  7445  ndmovass  7591  ndmovdistr  7592  extmptsuppeq  8169  funsssuppss  8171  eceqoveq  8812  supval2  9446  axpowndlem3  10590  adderpq  10947  mulerpq  10948  fzoval  13629  swrdnznd  14588  pfxnd0  14634  grpidval  18576  tgdif0  22486  resstopn  22681  rdgprc0  34753  bj-projval  35865  wl-nax6im  36375  itg2addnclem3  36529  or3or  42759  ndmafv  45834  nfunsnafv  45836  afvnufveq  45841  aovprc  45882  ndmaovass  45900  ndmaovdistr  45901  tz6.12-2-afv2  45931  naryfval  47267  naryfvalixp  47268
  Copyright terms: Public domain W3C validator