Theorem con2d 135

Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.)

Hypothesis

Ref	Expression
con2d.1	⊢ (𝜑 → (𝜓 → ¬ 𝜒))

Assertion

Ref	Expression
con2d	⊢ (𝜑 → (𝜒 → ¬ 𝜓))

Proof of Theorem con2d

Step	Hyp	Ref	Expression
1		notnotr 131	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con2d.1	. . 3 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
3	1, 2	syl5 35	. 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:  con2  136  mt2d  137  pm3.2im  161  exists2  2686  necon2bd  2971  spcimegf  3514  spcegf  3546  spcimedv  3549  rspcimedv  3567  disjxun  5100  exexneq  5402  sotric  5585  sotrieq  5586  poirr2  6112  dfpo2  6288  funun  6574  imadif  6612  soisoi  7324  onnminsb  7796  oneqmin  7797  ordunisuc2  7838  limsssuc  7844  tz7.48lemOLD  8429  sdomdif  9122  sdomdomtrfi  9194  domsdomtrfi  9195  pssinf  9231  unblem1  9262  supnub  9432  infnlb  9463  elirrv  9569  elirrvOLDOLD  9571  inf3lem6  9612  cantnflem1  9668  cardne  10018  cardsdomel  10027  carddom2  10030  cardmin2  10052  alephnbtwn  10122  infdif2  10259  fin4en1  10359  fin23lem31  10393  isf32lem5  10407  isf34lem4  10427  cfpwsdom  10641  fpwwe2  10700  addnidpi  10958  genpnnp  11062  btwnnz  12745  prime  12750  qsqueeze  13301  xralrple  13305  xmullem2  13365  xmulneg1  13369  ssfzoulel  13864  elfznelfzob  13878  bcval4  14419  seqcoll  14577  hashtpg  14598  swrd0  14776  fsumcvg  15846  fsumsplit  15875  fprodcvg  16065  fprodsplit  16101  dvdsle  16448  divalglem8  16538  bitsinv1lem  16579  2mulprm  16831  pockthg  17046  prmunb  17054  vdwlem6  17126  ramlb  17159  chnpof1  18766  gsumzsplit  20103  obselocv  21996  lindsenlbs  22119  opsrtoslem2  22327  psdmul  22449  elcls  23353  fbasrn  24165  ufilb  24187  ufilmax  24188  rnelfmlem  24233  alexsubALTlem4  24331  tsmssplit  24433  recld2  25096  logbgcd1irr  27086  fsumharmonic  27303  chtub  27503  lgsne0  27626  ltsres  27953  nosupbnd2lem1  28006  nocvxminlem  28074  ltslpss  28228  ltmuls2  28491  ltonold  28581  axlowdim  29473  wlkp1lem5  30190  wlkp1lem6  30191  cyclnspth  30323  eupth2lem3lem4  30766  cvnsym  32826  cvntr  32828  atcvati  32922  rmounid  33025  ballotlemfc0  35060  ballotlemfcc  35061  ballotlemfrcn0  35097  ballotlemirc  35099  acycgr2v  35836  cusgracyclt3v  35842  fmlasucdisj  36085  nmulprop  36861  nn0prpw  37033  onsucconni  37147  onint1  37159  icorempo  38194  relowlpssretop  38207  fvineqsneq  38255  poimirlem16  38474  poimirlem26  38484  fdc  38599  lsatcvat  40027  hlrelat2  40380  ltltncvr  40400  islln2a  40494  islpln2a  40525  islvol2aN  40569  dvrelog2b  43036  mullt0b2d  43476  rencldnfilem  43765  cantnfresb  44269  dflim5  44274  ss2iundf  44603  uneqsn  44969  radcnvrat  45242  stoweidlem34  46966  oddneven  48664