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  180  pm2.8  985  dedlem0b  1055  meredith  1660  ax12ev2  2214  necon3bd  2970  necon1bd  2974  spc2d  3561  sspss  4055  neldif  4087  ssonprc  7766  limsssuc  7826  limom  7858  onfununi  8307  pw2f1olem  9049  domtriord  9091  pssnn  9133  ordtypelem10  9472  rankxpsuc  9837  carden2a  9921  fidomtri2  9949  alephdom  10034  isf32lem12  10318  isfin1-3  10340  isfin7-2  10350  entric  10511  inttsk  10729  zeo  12656  zeo2  12657  xrlttri  13138  xaddf  13224  elfzonelfzo  13772  fzonfzoufzol  13774  elfznelfzo  13776  om2uzf1oi  13963  hashnfinnn0  14371  ruclem3  16248  sumodd  16405  bitsinv1lem  16458  sadcaddlem  16474  phiprmpw  16794  iserodd  16854  fldivp1  16916  prmpwdvds  16923  vdwlem6  17005  sylow2alem2  19641  efgs1b  19759  fctop  23044  cctop  23046  ppttop  23047  iccpnfcnv  24986  iccpnfhmeo  24987  iscau2  25319  ovolicc2lem2  25560  mbfeqalem1  25683  limccnp2  25934  radcnv0  26456  psercnlem1  26465  pserdvlem2  26468  logtayl  26702  cxpsqrt  26745  rlimcnp2  27008  amgm  27032  pntpbnd1  27627  pntlem3  27650  nolesgn2o  27712  nogesgn1o  27714  atssma  32527  fsuppcurry1  32876  fsuppcurry2  32877  supxrnemnf  32920  xrge0iifcnv  34191  eulerpartlemf  34628  onvf1odlem4  35413  cusgracyclt3v  35470  arg-ax  36740  pw2f1ocnv  43578  onsupnmax  43769  infordmin  44072  clsk1independent  44586  pm10.57  44911  con5  45062  con3ALT2  45070  xrred  45904  afvco2  47734  islininds2  49070