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  3543  spc3gv  3547  frpoind  6298  soisoi  7274  isomin  7283  riotaclb  7356  extmptsuppeq  8129  mpoxopynvov0g  8155  fsetcdmex  8801  boxcutc  8880  sdomel  9053  onsdominel  9055  preleqALT  9527  frind  9663  cflim2  10174  cfslbn  10178  cofsmo  10180  fincssdom  10234  fin23lem25  10235  fin23lem26  10236  fin1a2s  10325  pwfseqlem4  10574  ltapr  10957  suplem2pr  10965  qsqueeze  13117  ssfzoulel  13677  ssnn0fi  13909  hashbnd  14260  hashclb  14282  hashgt0elex  14325  hashgt12el  14346  hashgt12el2  14347  2mulprm  16621  pc2dvds  16808  infpnlem1  16839  mndpsuppss  18691  odcl2  19498  ufilmax  23850  ufileu  23862  filufint  23863  hausflim  23924  flimfnfcls  23971  alexsubALTlem3  23992  alexsubALTlem4  23993  reconnlem2  24771  lebnumlem3  24908  rrxmvallem  25349  itg1ge0a  25656  itg2seq  25687  m1lgs  27339  nosepon  27617  leadds1im  27967  leadds1  27969  oncutlt  28244  onnolt  28246  bdaypw2n0bndlem  28443  lmieu  28840  axlowdimlem14  29012  usgredg2v  29284  cusgrfilem3  29515  cusgrfi  29516  vtxdgoddnumeven  29611  clwwlknon1sn  30159  ex-natded5.13-2  30475  diffib  32580  ordtconnlem1  34074  eulerpartlemgh  34528  bnj23  34867  nn0prpw  36511  meran1  36599  finxpreclem6  37708  wl-spae  37837  poimirlem32  37964  heiborlem1  38123  riotaclbgBAD  39391  primrootspoweq0  42537  aks6d1c2p2  42550  hashscontpow  42553  aks6d1c5lem1  42567  aks6d1c6lem3  42603  ioin9i8  42638  onsupmaxb  43670  onsupsucismax  43710  tfsconcat0b  43777  relpmin  45382  reclt0  45823  limclr  46087  eu2ndop1stv  47559  requad01  48055  line2ylem  49185  line2xlem  49187