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  1642  ax12ev2  2187  necon3bd  2946  necon1bd  2950  spc2d  3556  sspss  4054  neldif  4086  ssonprc  7732  limsssuc  7792  limom  7824  onfununi  8273  pw2f1olem  9009  domtriord  9051  pssnn  9093  ordtypelem10  9432  rankxpsuc  9794  carden2a  9878  fidomtri2  9906  alephdom  9991  isf32lem12  10274  isfin1-3  10296  isfin7-2  10306  entric  10467  inttsk  10685  zeo  12578  zeo2  12579  xrlttri  13053  xaddf  13139  elfzonelfzo  13685  fzonfzoufzol  13687  elfznelfzo  13689  om2uzf1oi  13876  hashnfinnn0  14284  ruclem3  16158  sumodd  16315  bitsinv1lem  16368  sadcaddlem  16384  phiprmpw  16703  iserodd  16763  fldivp1  16825  prmpwdvds  16832  vdwlem6  16914  sylow2alem2  19547  efgs1b  19665  fctop  22948  cctop  22950  ppttop  22951  iccpnfcnv  24898  iccpnfhmeo  24899  iscau2  25233  ovolicc2lem2  25475  mbfeqalem1  25598  limccnp2  25849  radcnv0  26381  psercnlem1  26391  pserdvlem2  26394  logtayl  26625  cxpsqrt  26668  rlimcnp2  26932  amgm  26957  pntpbnd1  27553  pntlem3  27576  nolesgn2o  27639  nogesgn1o  27641  atssma  32453  fsuppcurry1  32803  fsuppcurry2  32804  supxrnemnf  32848  xrge0iifcnv  34090  eulerpartlemf  34527  onvf1odlem4  35300  cusgracyclt3v  35350  arg-ax  36610  pw2f1ocnv  43275  onsupnmax  43466  infordmin  43769  clsk1independent  44283  pm10.57  44608  con5  44759  con3ALT2  44767  xrred  45605  afvco2  47418  islininds2  48726