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  3560  spc3gv  3564  frpoind  6301  wfiOLD  6310  soisoi  7278  isomin  7287  riotaclb  7360  extmptsuppeq  8124  mpoxopynvov0g  8150  fsetcdmex  8808  boxcutc  8886  sdomel  9075  onsdominel  9077  preleqALT  9562  frind  9695  cflim2  10208  cfslbn  10212  cofsmo  10214  fincssdom  10268  fin23lem25  10269  fin23lem26  10270  fin1a2s  10359  pwfseqlem4  10607  ltapr  10990  suplem2pr  10998  qsqueeze  13130  ssfzoulel  13676  ssnn0fi  13900  hashbnd  14246  hashclb  14268  hashgt0elex  14311  hashgt12el  14332  hashgt12el2  14333  2mulprm  16580  pc2dvds  16762  infpnlem1  16793  odcl2  19361  ufilmax  23295  ufileu  23307  filufint  23308  hausflim  23369  flimfnfcls  23416  alexsubALTlem3  23437  alexsubALTlem4  23438  reconnlem2  24227  lebnumlem3  24363  rrxmvallem  24805  itg1ge0a  25113  itg2seq  25144  m1lgs  26773  nosepon  27050  sleadd1im  27339  sleadd1  27341  lmieu  27789  axlowdimlem14  27967  usgredg2v  28238  cusgrfilem3  28468  cusgrfi  28469  vtxdgoddnumeven  28564  clwwlknon1sn  29107  ex-natded5.13-2  29423  diffib  31512  ordtconnlem1  32594  eulerpartlemgh  33067  bnj23  33419  nn0prpw  34871  meran1  34959  finxpreclem6  35940  wl-spae  36053  poimirlem32  36183  heiborlem1  36343  riotaclbgBAD  37489  aks6d1c2p2  40622  ioin9i8  40698  onsupmaxb  41631  onsupsucismax  41672  tfsconcat0b  41739  reclt0  43746  limclr  44016  eu2ndop1stv  45477  requad01  45933  mndpsuppss  46567  line2ylem  46957  line2xlem  46959