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  2643  moanimlem  2648  moexexlem  2656  eueq3  3676  opprc1  4864  opprc2  4865  mosubopt  5495  tz6.12-2  6872  nfvres  6923  fvco4i  6987  fvmptex  7008  fvopab4ndm  7024  ressnop0  7156  csbriota  7391  ovprc  7457  ovprc1  7458  ovprc2  7459  ndmovass  7608  ndmovdistr  7609  extmptsuppeq  8190  funsssuppss  8192  eceqoveq  8826  supval2  9422  axpowndlem3  10601  adderpq  10958  mulerpq  10959  fzoval  13707  swrdnznd  14702  pfxnd0  14750  grpidval  18746  tgdif0  23201  resstopn  23395  prcinf  35585  fineqvnttrclselem1  35593  rdgprc0  36322  bj-projval  37691  wl-nax6im  38232  itg2addnclem3  38383  or3or  44809  ndmafv  47937  nfunsnafv  47939  afvnufveq  47944  aovprc  47985  ndmaovass  48003  ndmaovdistr  48004  tz6.12-2-afv2  48034  naryfval  49467  naryfvalixp  49468