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  1832  rexim  3070  spc2gv  3566  spc3gv  3570  frpoind  6315  soisoi  7303  isomin  7312  riotaclb  7385  extmptsuppeq  8167  mpoxopynvov0g  8193  fsetcdmex  8836  boxcutc  8914  sdomel  9088  onsdominel  9090  preleqALT  9570  frind  9703  cflim2  10216  cfslbn  10220  cofsmo  10222  fincssdom  10276  fin23lem25  10277  fin23lem26  10278  fin1a2s  10367  pwfseqlem4  10615  ltapr  10998  suplem2pr  11006  qsqueeze  13161  ssfzoulel  13721  ssnn0fi  13950  hashbnd  14301  hashclb  14323  hashgt0elex  14366  hashgt12el  14387  hashgt12el2  14388  2mulprm  16663  pc2dvds  16850  infpnlem1  16881  mndpsuppss  18692  odcl2  19495  ufilmax  23794  ufileu  23806  filufint  23807  hausflim  23868  flimfnfcls  23915  alexsubALTlem3  23936  alexsubALTlem4  23937  reconnlem2  24716  lebnumlem3  24862  rrxmvallem  25304  itg1ge0a  25612  itg2seq  25643  m1lgs  27299  nosepon  27577  sleadd1im  27894  sleadd1  27896  onscutlt  28165  onnolt  28167  lmieu  28711  axlowdimlem14  28882  usgredg2v  29154  cusgrfilem3  29385  cusgrfi  29386  vtxdgoddnumeven  29481  clwwlknon1sn  30029  ex-natded5.13-2  30345  diffib  32450  ordtconnlem1  33914  eulerpartlemgh  34369  bnj23  34708  nn0prpw  36311  meran1  36399  finxpreclem6  37384  wl-spae  37509  poimirlem32  37646  heiborlem1  37805  riotaclbgBAD  38947  primrootspoweq0  42094  aks6d1c2p2  42107  hashscontpow  42110  aks6d1c5lem1  42124  aks6d1c6lem3  42160  ioin9i8  42195  onsupmaxb  43228  onsupsucismax  43268  tfsconcat0b  43335  relpmin  44942  reclt0  45387  limclr  45653  eu2ndop1stv  47126  requad01  47622  line2ylem  48740  line2xlem  48742