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  2940  necon1bd  2944  spc2d  3571  sspss  4068  neldif  4100  ssonprc  7766  limsssuc  7829  limom  7861  onfununi  8313  pw2f1olem  9050  domtriord  9093  pssnn  9138  ordtypelem10  9487  rankxpsuc  9842  carden2a  9926  fidomtri2  9954  alephdom  10041  isf32lem12  10324  isfin1-3  10346  isfin7-2  10356  entric  10517  inttsk  10734  zeo  12627  zeo2  12628  xrlttri  13106  xaddf  13191  elfzonelfzo  13737  fzonfzoufzol  13738  elfznelfzo  13740  om2uzf1oi  13925  hashnfinnn0  14333  ruclem3  16208  sumodd  16365  bitsinv1lem  16418  sadcaddlem  16434  phiprmpw  16753  iserodd  16813  fldivp1  16875  prmpwdvds  16882  vdwlem6  16964  sylow2alem2  19555  efgs1b  19673  fctop  22898  cctop  22900  ppttop  22901  iccpnfcnv  24849  iccpnfhmeo  24850  iscau2  25184  ovolicc2lem2  25426  mbfeqalem1  25549  limccnp2  25800  radcnv0  26332  psercnlem1  26342  pserdvlem2  26345  logtayl  26576  cxpsqrt  26619  rlimcnp2  26883  amgm  26908  pntpbnd1  27504  pntlem3  27527  nolesgn2o  27590  nogesgn1o  27592  atssma  32314  fsuppcurry1  32655  fsuppcurry2  32656  supxrnemnf  32698  xrge0iifcnv  33930  eulerpartlemf  34368  onvf1odlem4  35100  cusgracyclt3v  35150  arg-ax  36411  pw2f1ocnv  43033  onsupnmax  43224  infordmin  43528  clsk1independent  44042  pm10.57  44367  con5  44519  con3ALT2  44527  xrred  45368  afvco2  47181  islininds2  48477