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  1864  rexim  3103  spc2gv  3554  spc3gv  3558  frpoind  6345  soisoi  7336  isomin  7345  riotaclb  7418  extmptsuppeq  8208  mpoxopynvov0g  8234  fsetcdmex  8888  boxcutc  8972  sdomel  9146  onsdominel  9148  preleqALT  9621  frind  9757  cflim2  10344  cfslbn  10348  cofsmo  10350  fincssdom  10404  fin23lem25  10405  fin23lem26  10406  fin1a2s  10495  pwfseqlem4  10750  ltapr  11133  suplem2pr  11141  qsqueeze  13334  ssfzoulel  13898  ssnn0fi  14131  hashbnd  14483  hashclb  14505  hashgt0elex  14548  hashgt12el  14570  hashgt12el2  14571  2mulprm  16873  pc2dvds  17062  infpnlem1  17093  mndpsuppss  18964  odcl2  19784  ufilmax  24231  ufileu  24243  filufint  24244  hausflim  24305  flimfnfcls  24352  alexsubALTlem3  24373  alexsubALTlem4  24374  reconnlem2  25152  lebnumlem3  25289  rrxmvallem  25730  itg1ge0a  26037  itg2seq  26068  m1lgs  27720  nosepon  28027  leadds1im  28378  leadds1  28380  oncutlt  28655  onnolt  28657  bdaypw2n0bndlem  28854  lmieu  29294  axlowdimlem14  29538  usgredg2v  29813  cusgrfilem3  30043  cusgrfi  30044  vtxdgoddnumeven  30139  clwwlknon1sn  30696  ex-natded5.13-2  31022  diffib  33164  ordtconnlem1  34602  eulerpartlemgh  35056  bnj23  35395  onprcf1acwevdlem1  35964  nn0prpw  37203  meran1  37291  mh-regprimbi  37425  finxpreclem6  38412  wl-spae  38546  poimirlem32  38663  heiborlem1  38838  riotaclbgBAD  40104  primrootspoweq0  43249  aks6d1c2p2  43262  hashscontpow  43265  aks6d1c5lem1  43279  aks6d1c6lem3  43315  ioin9i8  43352  onsupmaxb  44334  onsupsucismax  44374  tfsconcat0b  44441  relpmin  46035  reclt0  46495  limclr  46758  eu2ndop1stv  48288  requad01  48812  line2ylem  49956  line2xlem  49958