Theorem nsyl2 142

Description: A negated syllogism inference. (Contributed by NM, 26-Jun-1994.) (Proof shortened by Wolf Lammen, 14-Nov-2023.)

Hypotheses

Ref	Expression
nsyl2.1	⊢ (𝜑 → ¬ 𝜓)
nsyl2.2	⊢ (¬ 𝜒 → 𝜓)

Assertion

Ref	Expression
nsyl2	⊢ (𝜑 → 𝜒)

Proof of Theorem nsyl2

Step	Hyp	Ref	Expression
1		nsyl2.1	. . 3 ⊢ (𝜑 → ¬ 𝜓)
2		nsyl2.2	. . 3 ⊢ (¬ 𝜒 → 𝜓)
3	1, 2	nsyl3 139	. 2 ⊢ (¬ 𝜒 → ¬ 𝜑)
4	3	con4i 115	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:  con1i  148  oprcl  4862  epelg  5559  elfvdm  6950  ovrcl  7492  elfvov1  7493  elfvov2  7494  tfi  7898  limom  7927  oaabs2  8696  ecexr  8760  elpmi  8904  elmapex  8906  pmresg  8936  pmsspw  8943  ixpssmap2g  8993  ixpssmapg  8994  resixpfo  9002  infensuc  9212  pm54.43lem  10120  alephnbtwn  10189  cfpwsdom  10708  elbasfv  17437  elbasov  17438  restsspw  17652  homarcl  18253  isipodrs  18761  grpidval  18890  efgrelexlema  20014  subcmn  20102  dvdsrval  20642  elocv  22029  mvrf1  22348  pf1rcl  22722  matrcl  22782  restrcl  23530  ssrest  23549  iscnp2  23612  isfcls  24383  isnghm  25097  dchrrcl  27624  ltsval2  28070  ltsres  28076  clwwlknnn  30681  hmdmadj  32599  indispconn  36207  cvmtop1  36233  cvmtop2  36234  mrsub0  36489  mrsubf  36490  mrsubccat  36491  mrsubcn  36492  mrsubco  36494  mrsubvrs  36495  msubf  36505  mclsrcl  36534  dfon2lem7  36766  funpartlem  36921  rankeq1o  37147  bj-brrelex12ALT  38252  bj-fvimacnv0  38475  atbase  40612  llnbase  40832  lplnbase  40857  lvolbase  40901  lhpbase  41321  mapco2g  43991