Theorem con4d 115

Description: Deduction associated with con4 113. (Contributed by NM, 26-Mar-1995.)

Hypothesis

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

Assertion

Ref	Expression
con4d	⊢ (𝜑 → (𝜒 → 𝜓))

Proof of Theorem con4d

Step	Hyp	Ref	Expression
1		con4d.1	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ 𝜒))
2		con4 113	. 2 ⊢ ((¬ 𝜓 → ¬ 𝜒) → (𝜒 → 𝜓))
3	1, 2	syl 17	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:  mt4d  117  pm2.21d  121  con2d  134  con1d  145  impcon4bid  227  con4bid  317  aleximi  1832  rexim  3077  spc2gv  3579  spc3gv  3583  frpoind  6331  wfiOLD  6340  soisoi  7321  isomin  7330  riotaclb  7403  extmptsuppeq  8187  mpoxopynvov0g  8213  fsetcdmex  8877  boxcutc  8955  sdomel  9138  onsdominel  9140  preleqALT  9631  frind  9764  cflim2  10277  cfslbn  10281  cofsmo  10283  fincssdom  10337  fin23lem25  10338  fin23lem26  10339  fin1a2s  10428  pwfseqlem4  10676  ltapr  11059  suplem2pr  11067  qsqueeze  13217  ssfzoulel  13776  ssnn0fi  14003  hashbnd  14354  hashclb  14376  hashgt0elex  14419  hashgt12el  14440  hashgt12el2  14441  2mulprm  16712  pc2dvds  16899  infpnlem1  16930  mndpsuppss  18743  odcl2  19546  ufilmax  23845  ufileu  23857  filufint  23858  hausflim  23919  flimfnfcls  23966  alexsubALTlem3  23987  alexsubALTlem4  23988  reconnlem2  24767  lebnumlem3  24913  rrxmvallem  25356  itg1ge0a  25664  itg2seq  25695  m1lgs  27351  nosepon  27629  sleadd1im  27946  sleadd1  27948  onscutlt  28217  onnolt  28219  lmieu  28763  axlowdimlem14  28934  usgredg2v  29206  cusgrfilem3  29437  cusgrfi  29438  vtxdgoddnumeven  29533  clwwlknon1sn  30081  ex-natded5.13-2  30397  diffib  32502  ordtconnlem1  33955  eulerpartlemgh  34410  bnj23  34749  nn0prpw  36341  meran1  36429  finxpreclem6  37414  wl-spae  37539  poimirlem32  37676  heiborlem1  37835  riotaclbgBAD  38972  primrootspoweq0  42119  aks6d1c2p2  42132  hashscontpow  42135  aks6d1c5lem1  42149  aks6d1c6lem3  42185  ioin9i8  42258  onsupmaxb  43263  onsupsucismax  43303  tfsconcat0b  43370  relpmin  44977  reclt0  45418  limclr  45684  eu2ndop1stv  47154  requad01  47635  line2ylem  48731  line2xlem  48733