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 ⊢ (𝜑 → (𝜒 → 𝜓))

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:  mt4d  118  pm2.21d  122  con2d  135  con1d  146  impcon4bid  230  con4bid  320  aleximi  1865  rexim  3104  spc2gv  3555  spc3gv  3559  frpoind  6338  soisoi  7328  isomin  7337  riotaclb  7410  extmptsuppeq  8189  mpoxopynvov0g  8215  fsetcdmex  8869  boxcutc  8953  sdomel  9127  onsdominel  9129  preleqALT  9602  frind  9738  cflim2  10322  cfslbn  10326  cofsmo  10328  fincssdom  10382  fin23lem25  10383  fin23lem26  10384  fin1a2s  10473  pwfseqlem4  10728  ltapr  11111  suplem2pr  11119  qsqueeze  13312  ssfzoulel  13875  ssnn0fi  14108  hashbnd  14460  hashclb  14482  hashgt0elex  14525  hashgt12el  14547  hashgt12el2  14548  2mulprm  16848  pc2dvds  17037  infpnlem1  17068  mndpsuppss  18939  odcl2  19759  ufilmax  24206  ufileu  24218  filufint  24219  hausflim  24280  flimfnfcls  24327  alexsubALTlem3  24348  alexsubALTlem4  24349  reconnlem2  25127  lebnumlem3  25264  rrxmvallem  25705  itg1ge0a  26012  itg2seq  26043  m1lgs  27697  nosepon  28004  leadds1im  28355  leadds1  28357  oncutlt  28632  onnolt  28634  bdaypw2n0bndlem  28831  lmieu  29271  axlowdimlem14  29515  usgredg2v  29790  cusgrfilem3  30020  cusgrfi  30021  vtxdgoddnumeven  30116  clwwlknon1sn  30673  ex-natded5.13-2  30999  diffib  33099  ordtconnlem1  34538  eulerpartlemgh  34993  bnj23  35332  nn0prpw  37081  meran1  37169  mh-regprimbi  37303  finxpreclem6  38287  wl-spae  38421  poimirlem32  38538  heiborlem1  38713  riotaclbgBAD  39979  primrootspoweq0  43124  aks6d1c2p2  43137  hashscontpow  43140  aks6d1c5lem1  43154  aks6d1c6lem3  43190  ioin9i8  43227  onsupmaxb  44199  onsupsucismax  44239  tfsconcat0b  44306  relpmin  45894  reclt0  46346  limclr  46609  eu2ndop1stv  48139  requad01  48663  line2ylem  49807  line2xlem  49809