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  norassOLD  1536  aleximi  1835  spc2gv  3529  spc3gv  3533  frpoind  6230  wfiOLD  6239  soisoi  7179  isomin  7188  riotaclb  7254  extmptsuppeq  7975  mpoxopynvov0g  8001  fsetcdmex  8609  boxcutc  8687  sdomel  8860  onsdominel  8862  preleqALT  9305  frind  9439  cflim2  9950  cfslbn  9954  cofsmo  9956  fincssdom  10010  fin23lem25  10011  fin23lem26  10012  fin1a2s  10101  pwfseqlem4  10349  ltapr  10732  suplem2pr  10740  qsqueeze  12864  ssfzoulel  13409  ssnn0fi  13633  hashbnd  13978  hashclb  14001  hashgt0elex  14044  hashgt12el  14065  hashgt12el2  14066  2mulprm  16326  pc2dvds  16508  infpnlem1  16539  odcl2  19087  ufilmax  22966  ufileu  22978  filufint  22979  hausflim  23040  flimfnfcls  23087  alexsubALTlem3  23108  alexsubALTlem4  23109  reconnlem2  23896  lebnumlem3  24032  rrxmvallem  24473  itg1ge0a  24781  itg2seq  24812  m1lgs  26441  lmieu  27049  axlowdimlem14  27226  usgredg2v  27497  cusgrfilem3  27727  cusgrfi  27728  vtxdgoddnumeven  27823  clwwlknon1sn  28365  ex-natded5.13-2  28681  diffib  30770  ordtconnlem1  31776  eulerpartlemgh  32245  bnj23  32597  nosepon  33795  nn0prpw  34439  meran1  34527  finxpreclem6  35494  wl-spae  35607  poimirlem32  35736  heiborlem1  35896  riotaclbgBAD  36895  ioin9i8  40101  reclt0  42821  limclr  43086  eu2ndop1stv  44504  requad01  44961  mndpsuppss  45595  line2ylem  45985  line2xlem  45987