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  2641  moanimlem  2646  moexexlem  2654  eueq3  3672  opprc1  4860  opprc2  4861  mosubopt  5489  mosubott  5491  tz6.12-2  6903  nfvres  6954  fvco4i  7018  fvmptex  7039  fvopab4ndm  7055  ressnop0  7189  csbriota  7423  ovprc  7489  ovprc1  7490  ovprc2  7491  ndmovass  7641  ndmovdistr  7642  extmptsuppeq  8243  funsssuppss  8245  eceqoveq  8881  supval2  9484  axpowndlem3  10723  adderpq  11080  mulerpq  11081  fzoval  13834  swrdnznd  14832  pfxnd0  14880  grpidval  18890  tgdif0  23365  resstopn  23559  prcinf  35922  fineqvnttrclselem1  35930  rdgprc0  36770  bj-projval  38124  wl-nax6im  38718  itg2addnclem3  38859  or3or  45284  ndmafv  48483  nfunsnafv  48485  afvnufveq  48490  aovprc  48531  ndmaovass  48549  ndmaovdistr  48550  tz6.12-2-afv2  48580  naryfval  50071  naryfvalixp  50072