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  1635  necon3bd  2943  necon1bd  2947  spc2d  3586  sspss  4095  neldif  4126  ssonprc  7791  limsssuc  7855  limom  7887  onfununi  8362  pw2f1olem  9101  domtriord  9148  pssnn  9193  pssnnOLD  9290  ordtypelem10  9552  rankxpsuc  9907  carden2a  9991  fidomtri2  10019  alephdom  10106  isf32lem12  10389  isfin1-3  10411  isfin7-2  10421  entric  10582  inttsk  10799  zeo  12681  zeo2  12682  xrlttri  13153  xaddf  13238  elfzonelfzo  13770  fzonfzoufzol  13771  elfznelfzo  13773  om2uzf1oi  13954  hashnfinnn0  14356  ruclem3  16213  sumodd  16368  bitsinv1lem  16419  sadcaddlem  16435  phiprmpw  16748  iserodd  16807  fldivp1  16869  prmpwdvds  16876  vdwlem6  16958  sylow2alem2  19585  efgs1b  19703  fctop  22951  cctop  22953  ppttop  22954  iccpnfcnv  24913  iccpnfhmeo  24914  iscau2  25249  ovolicc2lem2  25491  mbfeqalem1  25614  limccnp2  25865  radcnv0  26397  psercnlem1  26407  pserdvlem2  26410  logtayl  26639  cxpsqrt  26682  rlimcnp2  26943  amgm  26968  pntpbnd1  27564  pntlem3  27587  nolesgn2o  27650  nogesgn1o  27652  atssma  32260  fsuppcurry1  32589  fsuppcurry2  32590  supxrnemnf  32620  xrge0iifcnv  33665  eulerpartlemf  34121  cusgracyclt3v  34897  arg-ax  36031  pw2f1ocnv  42600  onsupnmax  42798  infordmin  43104  clsk1independent  43618  pm10.57  43950  con5  44103  con3ALT2  44111  xrred  44885  afvco2  46694  islininds2  47738