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  1833  rexim  3077  spc2gv  3554  spc3gv  3558  frpoind  6300  soisoi  7274  isomin  7283  riotaclb  7356  extmptsuppeq  8130  mpoxopynvov0g  8156  fsetcdmex  8800  boxcutc  8879  sdomel  9052  onsdominel  9054  preleqALT  9526  frind  9662  cflim2  10173  cfslbn  10177  cofsmo  10179  fincssdom  10233  fin23lem25  10234  fin23lem26  10235  fin1a2s  10324  pwfseqlem4  10573  ltapr  10956  suplem2pr  10964  qsqueeze  13116  ssfzoulel  13676  ssnn0fi  13908  hashbnd  14259  hashclb  14281  hashgt0elex  14324  hashgt12el  14345  hashgt12el2  14346  2mulprm  16620  pc2dvds  16807  infpnlem1  16838  mndpsuppss  18690  odcl2  19494  ufilmax  23851  ufileu  23863  filufint  23864  hausflim  23925  flimfnfcls  23972  alexsubALTlem3  23993  alexsubALTlem4  23994  reconnlem2  24772  lebnumlem3  24918  rrxmvallem  25360  itg1ge0a  25668  itg2seq  25699  m1lgs  27355  nosepon  27633  leadds1im  27983  leadds1  27985  oncutlt  28260  onnolt  28262  bdaypw2n0bndlem  28459  lmieu  28856  axlowdimlem14  29028  usgredg2v  29300  cusgrfilem3  29531  cusgrfi  29532  vtxdgoddnumeven  29627  clwwlknon1sn  30175  ex-natded5.13-2  30491  diffib  32596  ordtconnlem1  34081  eulerpartlemgh  34535  bnj23  34874  nn0prpw  36517  meran1  36605  finxpreclem6  37597  wl-spae  37722  poimirlem32  37849  heiborlem1  38008  riotaclbgBAD  39210  primrootspoweq0  42356  aks6d1c2p2  42369  hashscontpow  42372  aks6d1c5lem1  42386  aks6d1c6lem3  42422  ioin9i8  42457  onsupmaxb  43477  onsupsucismax  43517  tfsconcat0b  43584  relpmin  45189  reclt0  45631  limclr  45895  eu2ndop1stv  47367  requad01  47863  line2ylem  48993  line2xlem  48995