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  3668  opprc1  4856  opprc2  4857  mosubopt  5481  mosubott  5483  tz6.12-2  6872  nfvres  6923  fvco4i  6987  fvmptex  7008  fvopab4ndm  7024  ressnop0  7157  csbriota  7392  ovprc  7458  ovprc1  7459  ovprc2  7460  ndmovass  7609  ndmovdistr  7610  extmptsuppeq  8205  funsssuppss  8207  eceqoveq  8843  supval2  9447  axpowndlem3  10684  adderpq  11041  mulerpq  11042  fzoval  13794  swrdnznd  14790  pfxnd0  14838  grpidval  18840  tgdif0  23310  resstopn  23504  prcinf  35781  fineqvnttrclselem1  35789  rdgprc0  36555  bj-projval  37909  wl-nax6im  38451  itg2addnclem3  38592  or3or  45023  ndmafv  48210  nfunsnafv  48212  afvnufveq  48217  aovprc  48258  ndmaovass  48276  ndmaovdistr  48277  tz6.12-2-afv2  48307  naryfval  49740  naryfvalixp  49741