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  1641  ax12ev2  2181  necon3bd  2939  necon1bd  2943  spc2d  3568  sspss  4065  neldif  4097  ssonprc  7763  limsssuc  7826  limom  7858  onfununi  8310  pw2f1olem  9045  domtriord  9087  pssnn  9132  ordtypelem10  9480  rankxpsuc  9835  carden2a  9919  fidomtri2  9947  alephdom  10034  isf32lem12  10317  isfin1-3  10339  isfin7-2  10349  entric  10510  inttsk  10727  zeo  12620  zeo2  12621  xrlttri  13099  xaddf  13184  elfzonelfzo  13730  fzonfzoufzol  13731  elfznelfzo  13733  om2uzf1oi  13918  hashnfinnn0  14326  ruclem3  16201  sumodd  16358  bitsinv1lem  16411  sadcaddlem  16427  phiprmpw  16746  iserodd  16806  fldivp1  16868  prmpwdvds  16875  vdwlem6  16957  sylow2alem2  19548  efgs1b  19666  fctop  22891  cctop  22893  ppttop  22894  iccpnfcnv  24842  iccpnfhmeo  24843  iscau2  25177  ovolicc2lem2  25419  mbfeqalem1  25542  limccnp2  25793  radcnv0  26325  psercnlem1  26335  pserdvlem2  26338  logtayl  26569  cxpsqrt  26612  rlimcnp2  26876  amgm  26901  pntpbnd1  27497  pntlem3  27520  nolesgn2o  27583  nogesgn1o  27585  atssma  32307  fsuppcurry1  32648  fsuppcurry2  32649  supxrnemnf  32691  xrge0iifcnv  33923  eulerpartlemf  34361  onvf1odlem4  35093  cusgracyclt3v  35143  arg-ax  36404  pw2f1ocnv  43026  onsupnmax  43217  infordmin  43521  clsk1independent  44035  pm10.57  44360  con5  44512  con3ALT2  44520  xrred  45361  afvco2  47177  islininds2  48473