Theorem nsyl5 162

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 161	. 2 ⊢ (¬ 𝜒 → 𝜓)
4	3	con1i 149	1 ⊢ (¬ 𝜓 → 𝜒)

Syntax hints:  ¬ wn 3   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is referenced by:  pm5.55  947  euor2  2634  moanimlem  2640  moexexlem  2648  eueq3  3622  opprc1  4780  opprc2  4781  mosubopt  5362  nfvres  6687  fvco4i  6746  fvmptex  6766  fvopab4ndm  6781  ressnop0  6899  csbriota  7116  ovprc  7181  ovprc1  7182  ovprc2  7183  ndmovass  7325  ndmovdistr  7326  extmptsuppeq  7855  funsssuppss  7857  eceqoveq  8405  supval2  8937  axpowndlem3  10044  adderpq  10401  mulerpq  10402  fzoval  13073  swrdnznd  14036  pfxnd0  14082  grpidval  17922  tgdif0  21677  resstopn  21871  rdgprc0  33270  bj-projval  34698  wl-nax6im  35188  itg2addnclem3  35375  or3or  41082  ndmafv  44049  nfunsnafv  44051  afvnufveq  44056  aovprc  44097  ndmaovass  44115  ndmaovdistr  44116  tz6.12-2-afv2  44146  naryfval  45392  naryfvalixp  45393