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  3079  spc2gv  3556  spc3gv  3560  frpoind  6308  soisoi  7284  isomin  7293  riotaclb  7366  extmptsuppeq  8140  mpoxopynvov0g  8166  fsetcdmex  8812  boxcutc  8891  sdomel  9064  onsdominel  9066  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  13128  ssfzoulel  13688  ssnn0fi  13920  hashbnd  14271  hashclb  14293  hashgt0elex  14336  hashgt12el  14357  hashgt12el2  14358  2mulprm  16632  pc2dvds  16819  infpnlem1  16850  mndpsuppss  18702  odcl2  19506  ufilmax  23863  ufileu  23875  filufint  23876  hausflim  23937  flimfnfcls  23984  alexsubALTlem3  24005  alexsubALTlem4  24006  reconnlem2  24784  lebnumlem3  24930  rrxmvallem  25372  itg1ge0a  25680  itg2seq  25711  m1lgs  27367  nosepon  27645  leadds1im  27995  leadds1  27997  oncutlt  28272  onnolt  28274  bdaypw2n0bndlem  28471  lmieu  28868  axlowdimlem14  29040  usgredg2v  29312  cusgrfilem3  29543  cusgrfi  29544  vtxdgoddnumeven  29639  clwwlknon1sn  30187  ex-natded5.13-2  30503  diffib  32607  ordtconnlem1  34101  eulerpartlemgh  34555  bnj23  34894  nn0prpw  36536  meran1  36624  finxpreclem6  37645  wl-spae  37770  poimirlem32  37897  heiborlem1  38056  riotaclbgBAD  39324  primrootspoweq0  42470  aks6d1c2p2  42483  hashscontpow  42486  aks6d1c5lem1  42500  aks6d1c6lem3  42536  ioin9i8  42571  onsupmaxb  43590  onsupsucismax  43630  tfsconcat0b  43697  relpmin  45302  reclt0  45743  limclr  46007  eu2ndop1stv  47479  requad01  47975  line2ylem  49105  line2xlem  49107