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  2218  necon3bd  2971  necon1bd  2975  spc2d  3559  sspss  4053  neldif  4084  ssonprc  7790  limsssuc  7850  limom  7882  onfununi  8334  pw2f1olem  9083  domtriord  9125  pssnn  9167  ordtypelem10  9503  rankxpsuc  9868  carden2a  9975  fidomtri2  10003  alephdom  10088  isf32lem12  10370  isfin1-3  10392  isfin7-2  10402  entric  10569  inttsk  10787  zeo  12711  zeo2  12712  xrlttri  13194  xaddf  13280  elfzonelfzo  13829  fzonfzoufzol  13831  elfznelfzo  13833  om2uzf1oi  14021  hashnfinnn0  14429  ruclem3  16327  sumodd  16484  bitsinv1lem  16537  sadcaddlem  16553  phiprmpw  16873  iserodd  16933  fldivp1  16995  prmpwdvds  17002  vdwlem6  17084  sylow2alem2  19751  efgs1b  19869  fctop  23235  cctop  23237  ppttop  23238  iccpnfcnv  25178  iccpnfhmeo  25179  iscau2  25511  ovolicc2lem2  25752  mbfeqalem1  25875  limccnp2  26126  radcnv0  26659  psercnlem1  26668  pserdvlem2  26671  logtayl  26905  cxpsqrt  26948  rlimcnp2  27211  amgm  27235  pntpbnd1  27830  pntlem3  27853  nolesgn2o  27915  nogesgn1o  27917  atssma  32867  fsuppcurry1  33203  fsuppcurry2  33204  supxrnemnf  33247  xrge0iifcnv  34451  eulerpartlemf  34889  onvf1odlem4  35711  cusgracyclt3v  35743  arg-ax  37043  pw2f1ocnv  43886  onsupnmax  44077  infordmin  44380  clsk1independent  44894  pm10.57  45203  con5  45353  con3ALT2  45361  xrred  46202  afvco2  48072  islininds2  49422