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 ⊢ (¬ 𝜓 → 𝜒)

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  963  euor2  2641  moanimlem  2646  moexexlem  2654  eueq3  3674  opprc1  4862  opprc2  4863  mosubopt  5493  tz6.12-2  6868  nfvres  6919  fvco4i  6983  fvmptex  7004  fvopab4ndm  7020  ressnop0  7150  csbriota  7382  ovprc  7448  ovprc1  7449  ovprc2  7450  ndmovass  7598  ndmovdistr  7599  extmptsuppeq  8180  funsssuppss  8182  eceqoveq  8816  supval2  9411  axpowndlem3  10579  adderpq  10936  mulerpq  10937  fzoval  13684  swrdnznd  14676  pfxnd0  14722  grpidval  18714  tgdif0  23149  resstopn  23343  prcinf  35526  fineqvnttrclselem1  35534  rdgprc0  36283  bj-projval  37652  wl-nax6im  38193  itg2addnclem3  38344  or3or  44769  ndmafv  47897  nfunsnafv  47899  afvnufveq  47904  aovprc  47945  ndmaovass  47963  ndmaovdistr  47964  tz6.12-2-afv2  47994  naryfval  49428  naryfvalixp  49429