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 ⊢ (𝜑 → (¬ 𝜒 → 𝜓))

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  147  mt3d  149  pm2.24d  152  con3d  153  pm2.61d  181  pm2.8  988  dedlem0b  1058  meredith  1664  ax12ev2  2218  necon3bd  2974  necon1bd  2978  spc2d  3564  sspss  4058  neldif  4090  ssonprc  7774  limsssuc  7834  limom  7866  onfununi  8316  pw2f1olem  9057  domtriord  9099  pssnn  9141  ordtypelem10  9477  rankxpsuc  9842  carden2a  9940  fidomtri2  9968  alephdom  10053  isf32lem12  10336  isfin1-3  10358  isfin7-2  10368  entric  10529  inttsk  10747  zeo  12673  zeo2  12674  xrlttri  13155  xaddf  13241  elfzonelfzo  13789  fzonfzoufzol  13791  elfznelfzo  13793  om2uzf1oi  13980  hashnfinnn0  14388  ruclem3  16279  sumodd  16436  bitsinv1lem  16489  sadcaddlem  16505  phiprmpw  16825  iserodd  16885  fldivp1  16947  prmpwdvds  16954  vdwlem6  17036  sylow2alem2  19679  efgs1b  19797  fctop  23122  cctop  23124  ppttop  23125  iccpnfcnv  25064  iccpnfhmeo  25065  iscau2  25397  ovolicc2lem2  25638  mbfeqalem1  25761  limccnp2  26012  radcnv0  26537  psercnlem1  26546  pserdvlem2  26549  logtayl  26783  cxpsqrt  26826  rlimcnp2  27089  amgm  27113  pntpbnd1  27708  pntlem3  27731  nolesgn2o  27793  nogesgn1o  27795  atssma  32639  fsuppcurry1  32981  fsuppcurry2  32982  supxrnemnf  33025  xrge0iifcnv  34240  eulerpartlemf  34677  onvf1odlem4  35461  cusgracyclt3v  35519  arg-ax  36789  pw2f1ocnv  43626  onsupnmax  43817  infordmin  44120  clsk1independent  44634  pm10.57  44945  con5  45096  con3ALT2  45104  xrred  45938  afvco2  47768  islininds2  49115