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  974  dedlem0b  1044  meredith  1640  ax12ev2  2179  necon3bd  2953  necon1bd  2957  spc2d  3601  sspss  4101  neldif  4133  ssonprc  7808  limsssuc  7872  limom  7904  onfununi  8382  pw2f1olem  9117  domtriord  9164  pssnn  9209  ordtypelem10  9568  rankxpsuc  9923  carden2a  10007  fidomtri2  10035  alephdom  10122  isf32lem12  10405  isfin1-3  10427  isfin7-2  10437  entric  10598  inttsk  10815  zeo  12706  zeo2  12707  xrlttri  13182  xaddf  13267  elfzonelfzo  13809  fzonfzoufzol  13810  elfznelfzo  13812  om2uzf1oi  13995  hashnfinnn0  14401  ruclem3  16270  sumodd  16426  bitsinv1lem  16479  sadcaddlem  16495  phiprmpw  16814  iserodd  16874  fldivp1  16936  prmpwdvds  16943  vdwlem6  17025  sylow2alem2  19637  efgs1b  19755  fctop  23012  cctop  23014  ppttop  23015  iccpnfcnv  24976  iccpnfhmeo  24977  iscau2  25312  ovolicc2lem2  25554  mbfeqalem1  25677  limccnp2  25928  radcnv0  26460  psercnlem1  26470  pserdvlem2  26473  logtayl  26703  cxpsqrt  26746  rlimcnp2  27010  amgm  27035  pntpbnd1  27631  pntlem3  27654  nolesgn2o  27717  nogesgn1o  27719  atssma  32398  fsuppcurry1  32737  fsuppcurry2  32738  supxrnemnf  32773  xrge0iifcnv  33933  eulerpartlemf  34373  cusgracyclt3v  35162  arg-ax  36418  pw2f1ocnv  43054  onsupnmax  43245  infordmin  43550  clsk1independent  44064  pm10.57  44395  con5  44547  con3ALT2  44555  xrred  45381  afvco2  47193  islininds2  48406