Theorem con4d 116

Description: Deduction associated with con4 114. (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 114	. 2 ⊢ ((¬ 𝜓 → ¬ 𝜒) → (𝜒 → 𝜓))
3	1, 2	syl 18	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  118  pm2.21d  122  con2d  135  con1d  146  impcon4bid  230  con4bid  320  aleximi  1855  rexim  3106  spc2gv  3562  spc3gv  3566  frpoind  6333  soisoi  7316  isomin  7325  riotaclb  7398  extmptsuppeq  8172  mpoxopynvov0g  8198  fsetcdmex  8848  boxcutc  8927  sdomel  9100  onsdominel  9102  preleqALT  9574  frind  9710  cflim2  10235  cfslbn  10239  cofsmo  10241  fincssdom  10295  fin23lem25  10296  fin23lem26  10297  fin1a2s  10386  pwfseqlem4  10635  ltapr  11018  suplem2pr  11026  qsqueeze  13218  ssfzoulel  13780  ssnn0fi  14012  hashbnd  14363  hashclb  14385  hashgt0elex  14428  hashgt12el  14449  hashgt12el2  14450  2mulprm  16741  pc2dvds  16929  infpnlem1  16960  mndpsuppss  18813  odcl2  19626  ufilmax  24025  ufileu  24037  filufint  24038  hausflim  24099  flimfnfcls  24146  alexsubALTlem3  24167  alexsubALTlem4  24168  reconnlem2  24946  lebnumlem3  25083  rrxmvallem  25524  itg1ge0a  25831  itg2seq  25862  m1lgs  27510  nosepon  27787  leadds1im  28138  leadds1  28140  oncutlt  28415  onnolt  28417  bdaypw2n0bndlem  28614  lmieu  29036  axlowdimlem14  29214  usgredg2v  29486  cusgrfilem3  29716  cusgrfi  29717  vtxdgoddnumeven  29812  clwwlknon1sn  30360  ex-natded5.13-2  30676  diffib  32777  ordtconnlem1  34231  eulerpartlemgh  34685  bnj23  35024  nn0prpw  36696  meran1  36784  mh-regprimbi  36918  finxpreclem6  37902  wl-spae  38036  poimirlem32  38163  heiborlem1  38322  riotaclbgBAD  39590  primrootspoweq0  42735  aks6d1c2p2  42748  hashscontpow  42751  aks6d1c5lem1  42765  aks6d1c6lem3  42801  ioin9i8  42836  onsupmaxb  43828  onsupsucismax  43868  tfsconcat0b  43935  relpmin  45526  reclt0  45964  limclr  46227  eu2ndop1stv  47717  requad01  48241  line2ylem  49382  line2xlem  49384