Theorem con1d 145

Description: A contraposition deduction. (Contributed by NM, 27-Dec-1992.)

Hypothesis

Ref	Expression
con1d.1	⊢ (𝜑 → (¬ 𝜓 → 𝜒))

Assertion

Ref	Expression
con1d	⊢ (𝜑 → (¬ 𝜒 → 𝜓))

Proof of Theorem con1d

Step	Hyp	Ref	Expression
1		con1d.1	. . 3 ⊢ (𝜑 → (¬ 𝜓 → 𝜒))
2		notnot 142	. . 3 ⊢ (𝜒 → ¬ ¬ 𝜒)
3	1, 2	syl6 35	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒))
4	3	con4d 115	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:  con1  146  mt3d  148  pm2.24d  151  con3d  152  pm2.61d  179  pm2.8  974  dedlem0b  1044  meredith  1642  ax12ev2  2183  necon3bd  2942  necon1bd  2946  spc2d  3557  sspss  4052  neldif  4084  ssonprc  7720  limsssuc  7780  limom  7812  onfununi  8261  pw2f1olem  8994  domtriord  9036  pssnn  9078  ordtypelem10  9413  rankxpsuc  9772  carden2a  9856  fidomtri2  9884  alephdom  9969  isf32lem12  10252  isfin1-3  10274  isfin7-2  10284  entric  10445  inttsk  10662  zeo  12556  zeo2  12557  xrlttri  13035  xaddf  13120  elfzonelfzo  13666  fzonfzoufzol  13668  elfznelfzo  13670  om2uzf1oi  13857  hashnfinnn0  14265  ruclem3  16139  sumodd  16296  bitsinv1lem  16349  sadcaddlem  16365  phiprmpw  16684  iserodd  16744  fldivp1  16806  prmpwdvds  16813  vdwlem6  16895  sylow2alem2  19528  efgs1b  19646  fctop  22917  cctop  22919  ppttop  22920  iccpnfcnv  24867  iccpnfhmeo  24868  iscau2  25202  ovolicc2lem2  25444  mbfeqalem1  25567  limccnp2  25818  radcnv0  26350  psercnlem1  26360  pserdvlem2  26363  logtayl  26594  cxpsqrt  26637  rlimcnp2  26901  amgm  26926  pntpbnd1  27522  pntlem3  27545  nolesgn2o  27608  nogesgn1o  27610  atssma  32353  fsuppcurry1  32702  fsuppcurry2  32703  supxrnemnf  32746  xrge0iifcnv  33941  eulerpartlemf  34378  onvf1odlem4  35138  cusgracyclt3v  35188  arg-ax  36449  pw2f1ocnv  43069  onsupnmax  43260  infordmin  43564  clsk1independent  44078  pm10.57  44403  con5  44554  con3ALT2  44562  xrred  45402  afvco2  47206  islininds2  48515