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  975  dedlem0b  1045  meredith  1643  ax12ev2  2188  necon3bd  2947  necon1bd  2951  spc2d  3545  sspss  4043  neldif  4075  ssonprc  7734  limsssuc  7794  limom  7826  onfununi  8274  pw2f1olem  9012  domtriord  9054  pssnn  9096  ordtypelem10  9435  rankxpsuc  9797  carden2a  9881  fidomtri2  9909  alephdom  9994  isf32lem12  10277  isfin1-3  10299  isfin7-2  10309  entric  10470  inttsk  10688  zeo  12606  zeo2  12607  xrlttri  13081  xaddf  13167  elfzonelfzo  13715  fzonfzoufzol  13717  elfznelfzo  13719  om2uzf1oi  13906  hashnfinnn0  14314  ruclem3  16191  sumodd  16348  bitsinv1lem  16401  sadcaddlem  16417  phiprmpw  16737  iserodd  16797  fldivp1  16859  prmpwdvds  16866  vdwlem6  16948  sylow2alem2  19584  efgs1b  19702  fctop  22979  cctop  22981  ppttop  22982  iccpnfcnv  24921  iccpnfhmeo  24922  iscau2  25254  ovolicc2lem2  25495  mbfeqalem1  25618  limccnp2  25869  radcnv0  26394  psercnlem1  26403  pserdvlem2  26406  logtayl  26637  cxpsqrt  26680  rlimcnp2  26943  amgm  26968  pntpbnd1  27563  pntlem3  27586  nolesgn2o  27649  nogesgn1o  27651  atssma  32464  fsuppcurry1  32812  fsuppcurry2  32813  supxrnemnf  32856  xrge0iifcnv  34093  eulerpartlemf  34530  onvf1odlem4  35304  cusgracyclt3v  35354  arg-ax  36614  pw2f1ocnv  43483  onsupnmax  43674  infordmin  43977  clsk1independent  44491  pm10.57  44816  con5  44967  con3ALT2  44975  xrred  45812  afvco2  47636  islininds2  48972