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  973  dedlem0b  1045  meredith  1639  ax12ev2  2181  necon3bd  2960  necon1bd  2964  spc2d  3615  sspss  4125  neldif  4157  ssonprc  7823  limsssuc  7887  limom  7919  onfununi  8397  pw2f1olem  9142  domtriord  9189  pssnn  9234  ordtypelem10  9596  rankxpsuc  9951  carden2a  10035  fidomtri2  10063  alephdom  10150  isf32lem12  10433  isfin1-3  10455  isfin7-2  10465  entric  10626  inttsk  10843  zeo  12729  zeo2  12730  xrlttri  13201  xaddf  13286  elfzonelfzo  13819  fzonfzoufzol  13820  elfznelfzo  13822  om2uzf1oi  14004  hashnfinnn0  14410  ruclem3  16281  sumodd  16436  bitsinv1lem  16487  sadcaddlem  16503  phiprmpw  16823  iserodd  16882  fldivp1  16944  prmpwdvds  16951  vdwlem6  17033  sylow2alem2  19660  efgs1b  19778  fctop  23032  cctop  23034  ppttop  23035  iccpnfcnv  24994  iccpnfhmeo  24995  iscau2  25330  ovolicc2lem2  25572  mbfeqalem1  25695  limccnp2  25947  radcnv0  26477  psercnlem1  26487  pserdvlem2  26490  logtayl  26720  cxpsqrt  26763  rlimcnp2  27027  amgm  27052  pntpbnd1  27648  pntlem3  27671  nolesgn2o  27734  nogesgn1o  27736  atssma  32410  fsuppcurry1  32739  fsuppcurry2  32740  supxrnemnf  32775  xrge0iifcnv  33879  eulerpartlemf  34335  cusgracyclt3v  35124  arg-ax  36382  pw2f1ocnv  42994  onsupnmax  43189  infordmin  43494  clsk1independent  44008  pm10.57  44340  con5  44493  con3ALT2  44501  xrred  45280  afvco2  47091  islininds2  48213