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  970  dedlem0b  1042  meredith  1644  necon3bd  2957  necon1bd  2961  spc2d  3541  sspss  4034  neldif  4064  ssonprc  7637  limsssuc  7697  limom  7728  onfununi  8172  pw2f1olem  8863  domtriord  8910  pssnn  8951  pssnnOLD  9040  ordtypelem10  9286  rankxpsuc  9640  carden2a  9724  fidomtri2  9752  alephdom  9837  isf32lem12  10120  isfin1-3  10142  isfin7-2  10152  entric  10313  inttsk  10530  zeo  12406  zeo2  12407  xrlttri  12873  xaddf  12958  elfzonelfzo  13489  fzonfzoufzol  13490  elfznelfzo  13492  om2uzf1oi  13673  hashnfinnn0  14076  ruclem3  15942  sumodd  16097  bitsinv1lem  16148  sadcaddlem  16164  phiprmpw  16477  iserodd  16536  fldivp1  16598  prmpwdvds  16605  vdwlem6  16687  sylow2alem2  19223  efgs1b  19342  fctop  22154  cctop  22156  ppttop  22157  iccpnfcnv  24107  iccpnfhmeo  24108  iscau2  24441  ovolicc2lem2  24682  mbfeqalem1  24805  limccnp2  25056  radcnv0  25575  psercnlem1  25584  pserdvlem2  25587  logtayl  25815  cxpsqrt  25858  rlimcnp2  26116  amgm  26140  pntpbnd1  26734  pntlem3  26757  atssma  30740  fsuppcurry1  31060  fsuppcurry2  31061  supxrnemnf  31091  xrge0iifcnv  31883  eulerpartlemf  32337  cusgracyclt3v  33118  nolesgn2o  33874  nogesgn1o  33876  arg-ax  34605  pw2f1ocnv  40859  infordmin  41139  clsk1independent  41656  pm10.57  41989  con5  42142  con3ALT2  42150  xrred  42904  afvco2  44668  islininds2  45825