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  2185  necon3bd  2943  necon1bd  2947  spc2d  3553  sspss  4051  neldif  4083  ssonprc  7726  limsssuc  7786  limom  7818  onfununi  8267  pw2f1olem  9001  domtriord  9043  pssnn  9085  ordtypelem10  9420  rankxpsuc  9782  carden2a  9866  fidomtri2  9894  alephdom  9979  isf32lem12  10262  isfin1-3  10284  isfin7-2  10294  entric  10455  inttsk  10672  zeo  12565  zeo2  12566  xrlttri  13040  xaddf  13125  elfzonelfzo  13671  fzonfzoufzol  13673  elfznelfzo  13675  om2uzf1oi  13862  hashnfinnn0  14270  ruclem3  16144  sumodd  16301  bitsinv1lem  16354  sadcaddlem  16370  phiprmpw  16689  iserodd  16749  fldivp1  16811  prmpwdvds  16818  vdwlem6  16900  sylow2alem2  19532  efgs1b  19650  fctop  22920  cctop  22922  ppttop  22923  iccpnfcnv  24870  iccpnfhmeo  24871  iscau2  25205  ovolicc2lem2  25447  mbfeqalem1  25570  limccnp2  25821  radcnv0  26353  psercnlem1  26363  pserdvlem2  26366  logtayl  26597  cxpsqrt  26640  rlimcnp2  26904  amgm  26929  pntpbnd1  27525  pntlem3  27548  nolesgn2o  27611  nogesgn1o  27613  atssma  32360  fsuppcurry1  32711  fsuppcurry2  32712  supxrnemnf  32755  xrge0iifcnv  33967  eulerpartlemf  34404  onvf1odlem4  35171  cusgracyclt3v  35221  arg-ax  36481  pw2f1ocnv  43154  onsupnmax  43345  infordmin  43649  clsk1independent  44163  pm10.57  44488  con5  44639  con3ALT2  44647  xrred  45487  afvco2  47300  islininds2  48609