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  2647  moanimlem  2652  moexexlem  2660  eueq3  3683  opprc1  4866  opprc2  4867  mosubopt  5494  tz6.12-2  6869  nfvres  6920  fvco4i  6984  fvmptex  7005  fvopab4ndm  7021  ressnop0  7151  csbriota  7383  ovprc  7449  ovprc1  7450  ovprc2  7451  ndmovass  7599  ndmovdistr  7600  extmptsuppeq  8184  funsssuppss  8186  eceqoveq  8820  supval2  9415  axpowndlem3  10584  adderpq  10941  mulerpq  10942  fzoval  13688  swrdnznd  14680  pfxnd0  14726  grpidval  18719  tgdif0  23118  resstopn  23312  prcinf  35449  fineqvnttrclselem1  35457  rdgprc0  36182  bj-projval  37520  wl-nax6im  38061  itg2addnclem3  38212  or3or  44641  ndmafv  47766  nfunsnafv  47768  afvnufveq  47773  aovprc  47814  ndmaovass  47832  ndmaovdistr  47833  tz6.12-2-afv2  47863  naryfval  49293  naryfvalixp  49294