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  226  con4bid  316  aleximi  1834  rexim  3086  spc2gv  3573  spc3gv  3577  frpoind  6316  wfiOLD  6325  soisoi  7293  isomin  7302  riotaclb  7375  extmptsuppeq  8139  mpoxopynvov0g  8165  fsetcdmex  8823  boxcutc  8901  sdomel  9090  onsdominel  9092  preleqALT  9577  frind  9710  cflim2  10223  cfslbn  10227  cofsmo  10229  fincssdom  10283  fin23lem25  10284  fin23lem26  10285  fin1a2s  10374  pwfseqlem4  10622  ltapr  11005  suplem2pr  11013  qsqueeze  13145  ssfzoulel  13691  ssnn0fi  13915  hashbnd  14261  hashclb  14283  hashgt0elex  14326  hashgt12el  14347  hashgt12el2  14348  2mulprm  16595  pc2dvds  16777  infpnlem1  16808  odcl2  19376  ufilmax  23310  ufileu  23322  filufint  23323  hausflim  23384  flimfnfcls  23431  alexsubALTlem3  23452  alexsubALTlem4  23453  reconnlem2  24242  lebnumlem3  24378  rrxmvallem  24820  itg1ge0a  25128  itg2seq  25159  m1lgs  26788  nosepon  27065  sleadd1im  27354  sleadd1  27356  lmieu  27823  axlowdimlem14  28001  usgredg2v  28272  cusgrfilem3  28502  cusgrfi  28503  vtxdgoddnumeven  28598  clwwlknon1sn  29141  ex-natded5.13-2  29457  diffib  31546  ordtconnlem1  32628  eulerpartlemgh  33101  bnj23  33453  nn0prpw  34905  meran1  34993  finxpreclem6  35974  wl-spae  36087  poimirlem32  36217  heiborlem1  36377  riotaclbgBAD  37522  aks6d1c2p2  40655  ioin9i8  40731  onsupmaxb  41664  onsupsucismax  41705  tfsconcat0b  41772  reclt0  43779  limclr  44049  eu2ndop1stv  45510  requad01  45966  mndpsuppss  46600  line2ylem  46990  line2xlem  46992