Theorem nsyl5 160

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

Step	Hyp	Ref	Expression
1		nsyl4.1	. . 3 ⊢ (𝜑 → 𝜓)
2		nsyl4.2	. . 3 ⊢ (¬ 𝜑 → 𝜒)
3	1, 2	nsyl4 159	. 2 ⊢ (¬ 𝜒 → 𝜓)
4	3	con1i 148	1 ⊢ (¬ 𝜓 → 𝜒)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  pm5.55  963  euor2  2638  moanimlem  2643  moexexlem  2651  eueq3  3669  opprc1  4857  opprc2  4858  mosubopt  5487  tz6.12-2  6866  nfvres  6917  fvco4i  6981  fvmptex  7002  fvopab4ndm  7018  ressnop0  7151  csbriota  7386  ovprc  7452  ovprc1  7453  ovprc2  7454  ndmovass  7603  ndmovdistr  7604  extmptsuppeq  8187  funsssuppss  8189  eceqoveq  8825  supval2  9428  axpowndlem3  10611  adderpq  10968  mulerpq  10969  fzoval  13718  swrdnznd  14713  pfxnd0  14761  grpidval  18757  tgdif0  23220  resstopn  23414  prcinf  35642  fineqvnttrclselem1  35650  rdgprc0  36373  bj-projval  37743  wl-nax6im  38284  itg2addnclem3  38425  or3or  44866  ndmafv  48031  nfunsnafv  48033  afvnufveq  48038  aovprc  48079  ndmaovass  48097  ndmaovdistr  48098  tz6.12-2-afv2  48128  naryfval  49561  naryfvalixp  49562