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  972  dedlem0b  1044  meredith  1644  necon3bd  2955  necon1bd  2959  spc2d  3593  sspss  4099  neldif  4129  ssonprc  7772  limsssuc  7836  limom  7868  onfununi  8338  pw2f1olem  9073  domtriord  9120  pssnn  9165  pssnnOLD  9262  ordtypelem10  9519  rankxpsuc  9874  carden2a  9958  fidomtri2  9986  alephdom  10073  isf32lem12  10356  isfin1-3  10378  isfin7-2  10388  entric  10549  inttsk  10766  zeo  12645  zeo2  12646  xrlttri  13115  xaddf  13200  elfzonelfzo  13731  fzonfzoufzol  13732  elfznelfzo  13734  om2uzf1oi  13915  hashnfinnn0  14318  ruclem3  16173  sumodd  16328  bitsinv1lem  16379  sadcaddlem  16395  phiprmpw  16706  iserodd  16765  fldivp1  16827  prmpwdvds  16834  vdwlem6  16916  sylow2alem2  19481  efgs1b  19599  fctop  22499  cctop  22501  ppttop  22502  iccpnfcnv  24452  iccpnfhmeo  24453  iscau2  24786  ovolicc2lem2  25027  mbfeqalem1  25150  limccnp2  25401  radcnv0  25920  psercnlem1  25929  pserdvlem2  25932  logtayl  26160  cxpsqrt  26203  rlimcnp2  26461  amgm  26485  pntpbnd1  27079  pntlem3  27102  nolesgn2o  27164  nogesgn1o  27166  atssma  31619  fsuppcurry1  31938  fsuppcurry2  31939  supxrnemnf  31969  xrge0iifcnv  32902  eulerpartlemf  33358  cusgracyclt3v  34136  arg-ax  35290  pw2f1ocnv  41762  onsupnmax  41963  infordmin  42269  clsk1independent  42783  pm10.57  43116  con5  43269  con3ALT2  43277  xrred  44062  afvco2  45871  islininds2  47119