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  180  pm2.8  980  dedlem0b  1050  meredith  1648  ax12ev2  2192  necon3bd  2949  necon1bd  2953  spc2d  3547  sspss  4040  neldif  4071  ssonprc  7737  limsssuc  7797  limom  7829  onfununi  8278  pw2f1olem  9016  domtriord  9058  pssnn  9100  ordtypelem10  9439  rankxpsuc  9804  carden2a  9888  fidomtri2  9916  alephdom  10001  isf32lem12  10284  isfin1-3  10306  isfin7-2  10316  entric  10477  inttsk  10695  zeo  12613  zeo2  12614  xrlttri  13088  xaddf  13174  elfzonelfzo  13722  fzonfzoufzol  13724  elfznelfzo  13726  om2uzf1oi  13913  hashnfinnn0  14321  ruclem3  16198  sumodd  16355  bitsinv1lem  16408  sadcaddlem  16424  phiprmpw  16744  iserodd  16804  fldivp1  16866  prmpwdvds  16873  vdwlem6  16955  sylow2alem2  19591  efgs1b  19709  fctop  22994  cctop  22996  ppttop  22997  iccpnfcnv  24936  iccpnfhmeo  24937  iscau2  25269  ovolicc2lem2  25510  mbfeqalem1  25633  limccnp2  25884  radcnv0  26406  psercnlem1  26415  pserdvlem2  26418  logtayl  26649  cxpsqrt  26692  rlimcnp2  26955  amgm  26979  pntpbnd1  27574  pntlem3  27597  nolesgn2o  27660  nogesgn1o  27662  atssma  32474  fsuppcurry1  32823  fsuppcurry2  32824  supxrnemnf  32867  xrge0iifcnv  34124  eulerpartlemf  34561  onvf1odlem4  35341  cusgracyclt3v  35391  arg-ax  36651  pw2f1ocnv  43489  onsupnmax  43680  infordmin  43983  clsk1independent  44497  pm10.57  44822  con5  44973  con3ALT2  44981  xrred  45816  afvco2  47646  islininds2  48982