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  2639  moanimlem  2644  moexexlem  2652  eueq3  3669  opprc1  4857  opprc2  4858  mosubopt  5482  mosubott  5484  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  38450  itg2addnclem3  38591  or3or  45022  ndmafv  48209  nfunsnafv  48211  afvnufveq  48216  aovprc  48257  ndmaovass  48275  ndmaovdistr  48276  tz6.12-2-afv2  48306  naryfval  49739  naryfvalixp  49740