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

Theorem nsyl5 162
 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 161 . 2 𝜒𝜓)
43con1i 149 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  946  euor2  2698  moanimlem  2704  moexexlem  2712  eueq3  3677  opprc1  4802  opprc2  4803  mosubopt  5377  nfvres  6688  fvco4i  6744  fvmptex  6764  fvopab4ndm  6779  ressnop0  6897  csbriota  7113  ovprc  7178  ovprc1  7179  ovprc2  7180  ndmovass  7321  ndmovdistr  7322  extmptsuppeq  7841  funsssuppss  7843  eceqoveq  8389  supval2  8907  axpowndlem3  10010  adderpq  10367  mulerpq  10368  fzoval  13034  swrdnznd  13995  pfxnd0  14041  grpidval  17862  tgdif0  21595  resstopn  21789  rdgprc0  33112  bj-projval  34393  wl-nax6im  34881  itg2addnclem3  35068  or3or  40657  ndmafv  43635  nfunsnafv  43637  afvnufveq  43642  aovprc  43683  ndmaovass  43701  ndmaovdistr  43702  tz6.12-2-afv2  43732  naryfval  44981  naryfvalixp  44982
 Copyright terms: Public domain W3C validator