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  2946  necon1bd  2950  spc2d  3544  sspss  4042  neldif  4074  ssonprc  7741  limsssuc  7801  limom  7833  onfununi  8281  pw2f1olem  9019  domtriord  9061  pssnn  9103  ordtypelem10  9442  rankxpsuc  9806  carden2a  9890  fidomtri2  9918  alephdom  10003  isf32lem12  10286  isfin1-3  10308  isfin7-2  10318  entric  10479  inttsk  10697  zeo  12615  zeo2  12616  xrlttri  13090  xaddf  13176  elfzonelfzo  13724  fzonfzoufzol  13726  elfznelfzo  13728  om2uzf1oi  13915  hashnfinnn0  14323  ruclem3  16200  sumodd  16357  bitsinv1lem  16410  sadcaddlem  16426  phiprmpw  16746  iserodd  16806  fldivp1  16868  prmpwdvds  16875  vdwlem6  16957  sylow2alem2  19593  efgs1b  19711  fctop  22969  cctop  22971  ppttop  22972  iccpnfcnv  24911  iccpnfhmeo  24912  iscau2  25244  ovolicc2lem2  25485  mbfeqalem1  25608  limccnp2  25859  radcnv0  26381  psercnlem1  26390  pserdvlem2  26393  logtayl  26624  cxpsqrt  26667  rlimcnp2  26930  amgm  26954  pntpbnd1  27549  pntlem3  27572  nolesgn2o  27635  nogesgn1o  27637  atssma  32449  fsuppcurry1  32797  fsuppcurry2  32798  supxrnemnf  32841  xrge0iifcnv  34077  eulerpartlemf  34514  onvf1odlem4  35288  cusgracyclt3v  35338  arg-ax  36598  pw2f1ocnv  43465  onsupnmax  43656  infordmin  43959  clsk1independent  44473  pm10.57  44798  con5  44949  con3ALT2  44957  xrred  45794  afvco2  47624  islininds2  48960