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  975  dedlem0b  1045  meredith  1643  ax12ev2  2188  necon3bd  2947  necon1bd  2951  spc2d  3558  sspss  4056  neldif  4088  ssonprc  7742  limsssuc  7802  limom  7834  onfununi  8283  pw2f1olem  9021  domtriord  9063  pssnn  9105  ordtypelem10  9444  rankxpsuc  9806  carden2a  9890  fidomtri2  9918  alephdom  10003  isf32lem12  10286  isfin1-3  10308  isfin7-2  10318  entric  10479  inttsk  10697  zeo  12590  zeo2  12591  xrlttri  13065  xaddf  13151  elfzonelfzo  13697  fzonfzoufzol  13699  elfznelfzo  13701  om2uzf1oi  13888  hashnfinnn0  14296  ruclem3  16170  sumodd  16327  bitsinv1lem  16380  sadcaddlem  16396  phiprmpw  16715  iserodd  16775  fldivp1  16837  prmpwdvds  16844  vdwlem6  16926  sylow2alem2  19559  efgs1b  19677  fctop  22960  cctop  22962  ppttop  22963  iccpnfcnv  24910  iccpnfhmeo  24911  iscau2  25245  ovolicc2lem2  25487  mbfeqalem1  25610  limccnp2  25861  radcnv0  26393  psercnlem1  26403  pserdvlem2  26406  logtayl  26637  cxpsqrt  26680  rlimcnp2  26944  amgm  26969  pntpbnd1  27565  pntlem3  27588  nolesgn2o  27651  nogesgn1o  27653  atssma  32465  fsuppcurry1  32813  fsuppcurry2  32814  supxrnemnf  32858  xrge0iifcnv  34110  eulerpartlemf  34547  onvf1odlem4  35319  cusgracyclt3v  35369  arg-ax  36629  pw2f1ocnv  43388  onsupnmax  43579  infordmin  43882  clsk1independent  44396  pm10.57  44721  con5  44872  con3ALT2  44880  xrred  45717  afvco2  47530  islininds2  48838