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  3559  sspss  4055  neldif  4087  ssonprc  7727  limsssuc  7790  limom  7822  onfununi  8271  pw2f1olem  9005  domtriord  9047  pssnn  9092  ordtypelem10  9438  rankxpsuc  9797  carden2a  9881  fidomtri2  9909  alephdom  9994  isf32lem12  10277  isfin1-3  10299  isfin7-2  10309  entric  10470  inttsk  10687  zeo  12580  zeo2  12581  xrlttri  13059  xaddf  13144  elfzonelfzo  13690  fzonfzoufzol  13691  elfznelfzo  13693  om2uzf1oi  13878  hashnfinnn0  14286  ruclem3  16160  sumodd  16317  bitsinv1lem  16370  sadcaddlem  16386  phiprmpw  16705  iserodd  16765  fldivp1  16827  prmpwdvds  16834  vdwlem6  16916  sylow2alem2  19515  efgs1b  19633  fctop  22907  cctop  22909  ppttop  22910  iccpnfcnv  24858  iccpnfhmeo  24859  iscau2  25193  ovolicc2lem2  25435  mbfeqalem1  25558  limccnp2  25809  radcnv0  26341  psercnlem1  26351  pserdvlem2  26354  logtayl  26585  cxpsqrt  26628  rlimcnp2  26892  amgm  26917  pntpbnd1  27513  pntlem3  27536  nolesgn2o  27599  nogesgn1o  27601  atssma  32340  fsuppcurry1  32681  fsuppcurry2  32682  supxrnemnf  32724  xrge0iifcnv  33899  eulerpartlemf  34337  onvf1odlem4  35078  cusgracyclt3v  35128  arg-ax  36389  pw2f1ocnv  43010  onsupnmax  43201  infordmin  43505  clsk1independent  44019  pm10.57  44344  con5  44496  con3ALT2  44504  xrred  45345  afvco2  47161  islininds2  48470