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  2663  necon2bd  2958  spcimegf  3519  spcegf  3521  spcimedv  3524  rspcimedv  3542  disjxun  5068  sotric  5522  sotrieq  5523  poirr2  6018  dfpo2  6188  funun  6464  imadif  6502  soisoi  7179  onnminsb  7626  oneqmin  7627  ordunisuc2  7666  limsssuc  7672  wfrlem10OLD  8120  tz7.48lem  8242  sdomdif  8861  pssinf  8962  unblem1  8996  supnub  9151  infnlb  9181  elirrv  9285  inf3lem6  9321  cantnflem1  9377  cardne  9654  cardsdomel  9663  carddom2  9666  cardmin2  9688  alephnbtwn  9758  infdif2  9897  fin4en1  9996  fin23lem31  10030  isf32lem5  10044  isf34lem4  10064  cfpwsdom  10271  fpwwe2  10330  addnidpi  10588  genpnnp  10692  btwnnz  12326  prime  12331  qsqueeze  12864  xralrple  12868  xmullem2  12928  xmulneg1  12932  ssfzoulel  13409  elfznelfzob  13421  bcval4  13949  seqcoll  14106  hashtpg  14127  swrd0  14299  fsumcvg  15352  fsumsplit  15381  fprodcvg  15568  fprodsplit  15604  dvdsle  15947  divalglem8  16037  bitsinv1lem  16076  2mulprm  16326  pockthg  16535  prmunb  16543  vdwlem6  16615  ramlb  16648  gsumzsplit  19443  obselocv  20845  opsrtoslem2  21173  elcls  22132  fbasrn  22943  ufilb  22965  ufilmax  22966  rnelfmlem  23011  alexsubALTlem4  23109  tsmssplit  23211  recld2  23883  logbgcd1irr  25849  fsumharmonic  26066  chtub  26265  lgsne0  26388  axlowdim  27232  wlkp1lem5  27947  wlkp1lem6  27948  cyclnspth  28069  eupth2lem3lem4  28496  cvnsym  30553  cvntr  30555  atcvati  30649  rmounid  30744  ballotlemfc0  32359  ballotlemfcc  32360  ballotlemfrcn0  32396  ballotlemirc  32398  acycgr2v  33012  cusgracyclt3v  33018  fmlasucdisj  33261  sltres  33792  nosupbnd2lem1  33845  nocvxminlem  33899  sltlpss  34014  nn0prpw  34439  onsucconni  34553  onint1  34565  icorempo  35449  relowlpssretop  35462  fvineqsneq  35510  lindsenlbs  35699  poimirlem16  35720  poimirlem26  35730  fdc  35830  lsatcvat  36991  hlrelat2  37344  ltltncvr  37364  islln2a  37458  islpln2a  37489  islvol2aN  37533  dvrelog2b  40002  rencldnfilem  40558  ss2iundf  41156  uneqsn  41522  radcnvrat  41821  stoweidlem34  43465  oddneven  44984