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  pm2.18OLD  129  con2d  136  con1d  147  impcon4bid  229  con4bid  319  norassOLD  1534  aleximi  1832  spc2gv  3603  spc3gv  3607  wfi  6183  soisoi  7083  isomin  7092  riotaclb  7157  extmptsuppeq  7856  mpoxopynvov0g  7882  boxcutc  8507  sdomel  8666  onsdominel  8668  preleqALT  9082  cflim2  9687  cfslbn  9691  cofsmo  9693  fincssdom  9747  fin23lem25  9748  fin23lem26  9749  fin1a2s  9838  pwfseqlem4  10086  ltapr  10469  suplem2pr  10477  qsqueeze  12597  ssfzoulel  13134  ssnn0fi  13356  hashbnd  13699  hashclb  13722  hashgt0elex  13765  hashgt12el  13786  hashgt12el2  13787  2mulprm  16039  pc2dvds  16217  infpnlem1  16248  odcl2  18694  ufilmax  22517  ufileu  22529  filufint  22530  hausflim  22591  flimfnfcls  22638  alexsubALTlem3  22659  alexsubALTlem4  22660  reconnlem2  23437  lebnumlem3  23569  rrxmvallem  24009  itg1ge0a  24314  itg2seq  24345  m1lgs  25966  lmieu  26572  axlowdimlem14  26743  usgredg2v  27011  cusgrfilem3  27241  cusgrfi  27242  vtxdgoddnumeven  27337  clwwlknon1sn  27881  ex-natded5.13-2  28197  ordtconnlem1  31169  eulerpartlemgh  31638  bnj23  31990  frpoind  33082  frind  33087  nosepon  33174  nn0prpw  33673  meran1  33761  finxpreclem6  34679  wl-spae  34763  poimirlem32  34926  heiborlem1  35091  riotaclbgBAD  36092  ioin9i8  39106  reclt0  41670  limclr  41943  eu2ndop1stv  43331  requad01  43793  mndpsuppss  44426  line2ylem  44745  line2xlem  44747