Theorem con1d 146

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 143	. . 3 ⊢ (𝜒 → ¬ ¬ 𝜒)
3	1, 2	syl6 36	. 2 ⊢ (𝜑 → (¬ 𝜓 → ¬ ¬ 𝜒))
4	3	con4d 116	1 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem is used by:  con1  147  mt3d  149  pm2.24d  152  con3d  153  pm2.61d  181  pm2.8  988  dedlem0b  1060  meredith  1674  ax12ev2  2219  necon3bd  2975  necon1bd  2979  spc2d  3564  sspss  4059  neldif  4091  ssonprc  7795  limsssuc  7855  limom  7887  onfununi  8337  pw2f1olem  9079  domtriord  9121  pssnn  9163  ordtypelem10  9499  rankxpsuc  9864  carden2a  9971  fidomtri2  9999  alephdom  10084  isf32lem12  10366  isfin1-3  10388  isfin7-2  10398  entric  10559  inttsk  10777  zeo  12700  zeo2  12701  xrlttri  13182  xaddf  13268  elfzonelfzo  13817  fzonfzoufzol  13819  elfznelfzo  13821  om2uzf1oi  14009  hashnfinnn0  14417  ruclem3  16314  sumodd  16471  bitsinv1lem  16524  sadcaddlem  16540  phiprmpw  16860  iserodd  16920  fldivp1  16982  prmpwdvds  16989  vdwlem6  17071  sylow2alem2  19719  efgs1b  19837  fctop  23198  cctop  23200  ppttop  23201  iccpnfcnv  25140  iccpnfhmeo  25141  iscau2  25473  ovolicc2lem2  25714  mbfeqalem1  25837  limccnp2  26088  radcnv0  26616  psercnlem1  26625  pserdvlem2  26628  logtayl  26862  cxpsqrt  26905  rlimcnp2  27168  amgm  27192  pntpbnd1  27787  pntlem3  27810  nolesgn2o  27872  nogesgn1o  27874  atssma  32767  fsuppcurry1  33106  fsuppcurry2  33107  supxrnemnf  33150  xrge0iifcnv  34354  eulerpartlemf  34792  onvf1odlem4  35614  cusgracyclt3v  35669  arg-ax  36968  pw2f1ocnv  43805  onsupnmax  43996  infordmin  44299  clsk1independent  44813  pm10.57  45122  con5  45272  con3ALT2  45280  xrred  46121  afvco2  47954  islininds2  49305