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  969  dedlem0b  1041  meredith  1645  necon3bd  2956  necon1bd  2960  spc2d  3531  sspss  4030  neldif  4060  ssonprc  7614  limsssuc  7672  limom  7703  onfununi  8143  pw2f1olem  8816  domtriord  8859  pssnn  8913  pssnnOLD  8969  ordtypelem10  9216  rankxpsuc  9571  carden2a  9655  fidomtri2  9683  alephdom  9768  isf32lem12  10051  isfin1-3  10073  isfin7-2  10083  entric  10244  inttsk  10461  zeo  12336  zeo2  12337  xrlttri  12802  xaddf  12887  elfzonelfzo  13417  fzonfzoufzol  13418  elfznelfzo  13420  om2uzf1oi  13601  hashnfinnn0  14004  ruclem3  15870  sumodd  16025  bitsinv1lem  16076  sadcaddlem  16092  phiprmpw  16405  iserodd  16464  fldivp1  16526  prmpwdvds  16533  vdwlem6  16615  sylow2alem2  19138  efgs1b  19257  fctop  22062  cctop  22064  ppttop  22065  iccpnfcnv  24013  iccpnfhmeo  24014  iscau2  24346  ovolicc2lem2  24587  mbfeqalem1  24710  limccnp2  24961  radcnv0  25480  psercnlem1  25489  pserdvlem2  25492  logtayl  25720  cxpsqrt  25763  rlimcnp2  26021  amgm  26045  pntpbnd1  26639  pntlem3  26662  atssma  30641  fsuppcurry1  30962  fsuppcurry2  30963  supxrnemnf  30993  xrge0iifcnv  31785  eulerpartlemf  32237  cusgracyclt3v  33018  nolesgn2o  33801  nogesgn1o  33803  arg-ax  34532  pw2f1ocnv  40775  infordmin  41037  clsk1independent  41545  pm10.57  41878  con5  42031  con3ALT2  42039  xrred  42794  afvco2  44555  islininds2  45713