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  3105  spc2gv  3557  spc3gv  3561  frpoind  6344  soisoi  7333  isomin  7342  riotaclb  7415  extmptsuppeq  8190  mpoxopynvov0g  8216  fsetcdmex  8868  boxcutc  8952  sdomel  9126  onsdominel  9128  preleqALT  9600  frind  9736  cflim2  10269  cfslbn  10273  cofsmo  10275  fincssdom  10329  fin23lem25  10330  fin23lem26  10331  fin1a2s  10420  pwfseqlem4  10675  ltapr  11058  suplem2pr  11066  qsqueeze  13257  ssfzoulel  13820  ssnn0fi  14053  hashbnd  14404  hashclb  14426  hashgt0elex  14469  hashgt12el  14491  hashgt12el2  14492  2mulprm  16789  pc2dvds  16977  infpnlem1  17008  mndpsuppss  18878  odcl2  19698  ufilmax  24139  ufileu  24151  filufint  24152  hausflim  24213  flimfnfcls  24260  alexsubALTlem3  24281  alexsubALTlem4  24282  reconnlem2  25060  lebnumlem3  25197  rrxmvallem  25638  itg1ge0a  25945  itg2seq  25976  m1lgs  27632  nosepon  27909  leadds1im  28260  leadds1  28262  oncutlt  28537  onnolt  28539  bdaypw2n0bndlem  28736  lmieu  29176  axlowdimlem14  29420  usgredg2v  29695  cusgrfilem3  29925  cusgrfi  29926  vtxdgoddnumeven  30021  clwwlknon1sn  30578  ex-natded5.13-2  30904  diffib  33004  ordtconnlem1  34442  eulerpartlemgh  34897  bnj23  35236  nn0prpw  36950  meran1  37038  mh-regprimbi  37172  finxpreclem6  38158  wl-spae  38292  poimirlem32  38409  heiborlem1  38569  riotaclbgBAD  39835  primrootspoweq0  42980  aks6d1c2p2  42993  hashscontpow  42996  aks6d1c5lem1  43010  aks6d1c6lem3  43046  ioin9i8  43083  onsupmaxb  44088  onsupsucismax  44128  tfsconcat0b  44195  relpmin  45783  reclt0  46228  limclr  46491  eu2ndop1stv  48021  requad01  48545  line2ylem  49689  line2xlem  49691