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  1834  rexim  3078  spc2gv  3542  spc3gv  3546  frpoind  6306  soisoi  7283  isomin  7292  riotaclb  7365  extmptsuppeq  8138  mpoxopynvov0g  8164  fsetcdmex  8810  boxcutc  8889  sdomel  9062  onsdominel  9064  preleqALT  9538  frind  9674  cflim2  10185  cfslbn  10189  cofsmo  10191  fincssdom  10245  fin23lem25  10246  fin23lem26  10247  fin1a2s  10336  pwfseqlem4  10585  ltapr  10968  suplem2pr  10976  qsqueeze  13153  ssfzoulel  13715  ssnn0fi  13947  hashbnd  14298  hashclb  14320  hashgt0elex  14363  hashgt12el  14384  hashgt12el2  14385  2mulprm  16662  pc2dvds  16850  infpnlem1  16881  mndpsuppss  18733  odcl2  19540  ufilmax  23872  ufileu  23884  filufint  23885  hausflim  23946  flimfnfcls  23993  alexsubALTlem3  24014  alexsubALTlem4  24015  reconnlem2  24793  lebnumlem3  24930  rrxmvallem  25371  itg1ge0a  25678  itg2seq  25709  m1lgs  27351  nosepon  27629  leadds1im  27979  leadds1  27981  oncutlt  28256  onnolt  28258  bdaypw2n0bndlem  28455  lmieu  28852  axlowdimlem14  29024  usgredg2v  29296  cusgrfilem3  29526  cusgrfi  29527  vtxdgoddnumeven  29622  clwwlknon1sn  30170  ex-natded5.13-2  30486  diffib  32591  ordtconnlem1  34068  eulerpartlemgh  34522  bnj23  34861  nn0prpw  36505  meran1  36593  mh-regprimbi  36727  finxpreclem6  37712  wl-spae  37846  poimirlem32  37973  heiborlem1  38132  riotaclbgBAD  39400  primrootspoweq0  42545  aks6d1c2p2  42558  hashscontpow  42561  aks6d1c5lem1  42575  aks6d1c6lem3  42611  ioin9i8  42646  onsupmaxb  43667  onsupsucismax  43707  tfsconcat0b  43774  relpmin  45379  reclt0  45820  limclr  46083  eu2ndop1stv  47573  requad01  48097  line2ylem  49227  line2xlem  49229