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  2216  necon3bd  2970  necon1bd  2974  spc2d  3557  sspss  4050  neldif  4081  ssonprc  7790  limsssuc  7850  limom  7882  onfununi  8333  pw2f1olem  9084  domtriord  9126  pssnn  9168  ordtypelem10  9505  rankxpsuc  9880  carden2a  10028  fidomtri2  10056  alephdom  10141  isf32lem12  10423  isfin1-3  10445  isfin7-2  10455  entric  10622  inttsk  10840  zeo  12766  zeo2  12767  xrlttri  13249  xaddf  13335  elfzonelfzo  13884  fzonfzoufzol  13886  elfznelfzo  13888  om2uzf1oi  14076  hashnfinnn0  14485  ruclem3  16381  sumodd  16538  bitsinv1lem  16591  sadcaddlem  16607  phiprmpw  16933  iserodd  16993  fldivp1  17055  prmpwdvds  17062  vdwlem6  17144  sylow2alem2  19812  efgs1b  19930  fctop  23302  cctop  23304  ppttop  23305  iccpnfcnv  25245  iccpnfhmeo  25246  iscau2  25578  ovolicc2lem2  25819  mbfeqalem1  25942  limccnp2  26192  radcnv0  26725  psercnlem1  26734  pserdvlem2  26737  logtayl  26970  cxpsqrt  27013  rlimcnp2  27276  amgm  27300  pntpbnd1  27895  pntlem3  27918  nolesgn2o  28010  nogesgn1o  28012  atssma  32962  fsuppcurry1  33298  fsuppcurry2  33299  supxrnemnf  33342  xrge0iifcnv  34547  eulerpartlemf  34985  onvf1odlem4  35858  cusgracyclt3v  35890  arg-ax  37174  pw2f1ocnv  43997  onsupnmax  44188  infordmin  44491  clsk1independent  45005  pm10.57  45314  con5  45464  con3ALT2  45472  xrred  46320  afvco2  48190  islininds2  49540