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  2973  necon1bd  2977  spc2d  3560  sspss  4032  neldif  4073  ssonprc  7825  limsssuc  7885  limom  7917  onfununi  8377  pw2f1olem  9128  domtriord  9170  pssnn  9212  ordtypelem10  9548  rankxpsuc  9926  carden2a  10074  fidomtri2  10102  alephdom  10187  isf32lem12  10469  isfin1-3  10491  isfin7-2  10501  entric  10668  inttsk  10886  zeo  12812  zeo2  12813  xrlttri  13295  xaddf  13381  elfzonelfzo  13931  fzonfzoufzol  13933  elfznelfzo  13935  om2uzf1oi  14123  hashnfinnn0  14532  ruclem3  16430  sumodd  16587  bitsinv1lem  16640  sadcaddlem  16656  phiprmpw  16982  iserodd  17042  fldivp1  17104  prmpwdvds  17111  vdwlem6  17193  sylow2alem2  19862  efgs1b  19980  fctop  23352  cctop  23354  ppttop  23355  iccpnfcnv  25295  iccpnfhmeo  25296  iscau2  25628  ovolicc2lem2  25869  mbfeqalem1  25992  limccnp2  26242  radcnv0  26773  psercnlem1  26782  pserdvlem2  26785  logtayl  27018  cxpsqrt  27061  rlimcnp2  27324  amgm  27348  pntpbnd1  27943  pntlem3  27966  nolesgn2o  28058  nogesgn1o  28060  atssma  33010  fsuppcurry1  33386  fsuppcurry2  33387  supxrnemnf  33430  xrge0iifcnv  34635  eulerpartlemf  35072  onvf1odlem4  36034  cusgracyclt3v  36078  arg-ax  37382  pw2f1ocnv  44237  onsupnmax  44422  infordmin  44725  clsk1independent  45238  pm10.57  45547  con5  45696  con3ALT2  45704  xrred  46581  afvco2  48451  islininds2  49801