Theorem con2d 134

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 130	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con2d.1	. . 3 ⊢ (𝜑 → (𝜓 → ¬ 𝜒))
3	1, 2	syl5 34	. 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:  con2  135  mt2d  136  pm3.2im  160  exists2  2659  necon2bd  2946  spcimegf  3506  spcegf  3544  spcimedv  3547  rspcimedv  3565  disjxun  5093  exexneq  5381  sotric  5559  sotrieq  5560  poirr2  6078  dfpo2  6251  funun  6535  imadif  6573  soisoi  7271  onnminsb  7741  oneqmin  7742  ordunisuc2  7783  limsssuc  7789  tz7.48lem  8369  sdomdif  9048  sdomdomtrfi  9120  domsdomtrfi  9121  pssinf  9156  unblem1  9186  supnub  9356  infnlb  9387  elirrvOLD  9494  inf3lem6  9533  cantnflem1  9589  cardne  9868  cardsdomel  9877  carddom2  9880  cardmin2  9902  alephnbtwn  9972  infdif2  10110  fin4en1  10210  fin23lem31  10244  isf32lem5  10258  isf34lem4  10278  cfpwsdom  10485  fpwwe2  10544  addnidpi  10802  genpnnp  10906  btwnnz  12559  prime  12564  qsqueeze  13110  xralrple  13114  xmullem2  13174  xmulneg1  13178  ssfzoulel  13670  elfznelfzob  13684  bcval4  14224  seqcoll  14381  hashtpg  14402  swrd0  14576  fsumcvg  15629  fsumsplit  15658  fprodcvg  15847  fprodsplit  15883  dvdsle  16231  divalglem8  16321  bitsinv1lem  16362  2mulprm  16614  pockthg  16828  prmunb  16836  vdwlem6  16908  ramlb  16941  chnpof1  18546  gsumzsplit  19849  obselocv  21675  opsrtoslem2  22001  psdmul  22091  elcls  22998  fbasrn  23809  ufilb  23831  ufilmax  23832  rnelfmlem  23877  alexsubALTlem4  23975  tsmssplit  24077  recld2  24740  logbgcd1irr  26741  fsumharmonic  26959  chtub  27160  lgsne0  27283  sltres  27611  nosupbnd2lem1  27664  nocvxminlem  27727  sltlpss  27863  sltmul2  28120  sltonold  28208  axlowdim  28950  wlkp1lem5  29665  wlkp1lem6  29666  cyclnspth  29790  eupth2lem3lem4  30222  cvnsym  32281  cvntr  32283  atcvati  32377  rmounid  32485  ballotlemfc0  34517  ballotlemfcc  34518  ballotlemfrcn0  34554  ballotlemirc  34556  acycgr2v  35205  cusgracyclt3v  35211  fmlasucdisj  35454  nn0prpw  36378  onsucconni  36492  onint1  36504  icorempo  37406  relowlpssretop  37419  fvineqsneq  37467  lindsenlbs  37665  poimirlem16  37686  poimirlem26  37696  fdc  37795  lsatcvat  39159  hlrelat2  39512  ltltncvr  39532  islln2a  39626  islpln2a  39657  islvol2aN  39701  dvrelog2b  42169  mullt0b2d  42592  rencldnfilem  42927  cantnfresb  43431  dflim5  43436  ss2iundf  43766  uneqsn  44132  radcnvrat  44421  stoweidlem34  46146  oddneven  47758