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  1673  ax12ev2  2215  necon3bd  2969  necon1bd  2973  spc2d  3556  sspss  4029  neldif  4070  ssonprc  7801  limsssuc  7861  limom  7893  onfununi  8352  pw2f1olem  9103  domtriord  9145  pssnn  9187  ordtypelem10  9524  rankxpsuc  9902  carden2a  10050  fidomtri2  10078  alephdom  10163  isf32lem12  10445  isfin1-3  10467  isfin7-2  10477  entric  10644  inttsk  10862  zeo  12788  zeo2  12789  xrlttri  13271  xaddf  13357  elfzonelfzo  13907  fzonfzoufzol  13909  elfznelfzo  13911  om2uzf1oi  14099  hashnfinnn0  14508  ruclem3  16406  sumodd  16563  bitsinv1lem  16616  sadcaddlem  16632  phiprmpw  16958  iserodd  17018  fldivp1  17080  prmpwdvds  17087  vdwlem6  17169  sylow2alem2  19837  efgs1b  19955  fctop  23327  cctop  23329  ppttop  23330  iccpnfcnv  25270  iccpnfhmeo  25271  iscau2  25603  ovolicc2lem2  25844  mbfeqalem1  25967  limccnp2  26217  radcnv0  26748  psercnlem1  26757  pserdvlem2  26760  logtayl  26993  cxpsqrt  27036  rlimcnp2  27299  amgm  27323  pntpbnd1  27918  pntlem3  27941  nolesgn2o  28033  nogesgn1o  28035  atssma  32985  fsuppcurry1  33362  fsuppcurry2  33363  supxrnemnf  33406  xrge0iifcnv  34611  eulerpartlemf  35048  onvf1odlem4  35953  cusgracyclt3v  35997  arg-ax  37296  pw2f1ocnv  44137  onsupnmax  44323  infordmin  44626  clsk1independent  45139  pm10.57  45448  con5  45598  con3ALT2  45606  xrred  46469  afvco2  48339  islininds2  49689