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  951  euor2  2613  moanimlem  2618  moexexlem  2626  eueq3  3717  opprc1  4897  opprc2  4898  mosubopt  5515  nfvres  6947  fvco4i  7010  fvmptex  7030  fvopab4ndm  7046  ressnop0  7173  csbriota  7403  ovprc  7469  ovprc1  7470  ovprc2  7471  ndmovass  7621  ndmovdistr  7622  extmptsuppeq  8213  funsssuppss  8215  eceqoveq  8862  supval2  9495  axpowndlem3  10639  adderpq  10996  mulerpq  10997  fzoval  13700  swrdnznd  14680  pfxnd0  14726  grpidval  18674  tgdif0  22999  resstopn  23194  prcinf  35108  rdgprc0  35794  bj-projval  36997  wl-nax6im  37519  itg2addnclem3  37680  or3or  44036  ndmafv  47152  nfunsnafv  47154  afvnufveq  47159  aovprc  47200  ndmaovass  47218  ndmaovdistr  47219  tz6.12-2-afv2  47249  naryfval  48549  naryfvalixp  48550
  Copyright terms: Public domain W3C validator