MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  con2d Structured version   Visualization version   GIF version

Theorem con2d 136
Description: A contraposition deduction. (Contributed by NM, 19-Aug-1993.)
Hypothesis
Ref Expression
con2d.1 (𝜑 → (𝜓 → ¬ 𝜒))
Assertion
Ref Expression
con2d (𝜑 → (𝜒 → ¬ 𝜓))

Proof of Theorem con2d
StepHypRef Expression
1 notnotr 132 . . 3 (¬ ¬ 𝜓𝜓)
2 con2d.1 . . 3 (𝜑 → (𝜓 → ¬ 𝜒))
31, 2syl5 34 . 2 (𝜑 → (¬ ¬ 𝜓 → ¬ 𝜒))
43con4d 115 1 (𝜑 → (𝜒 → ¬ 𝜓))
Colors of variables: wff setvar class
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  137  mt2d  138  pm3.2im  162  exists2  2742  necon2bd  3029  spcimegf  3586  spcegf  3588  spcimedv  3591  rspcimedv  3611  disjxun  5055  sotric  5494  sotrieq  5495  poirr2  5977  funun  6393  imadif  6431  soisoi  7070  onnminsb  7508  oneqmin  7509  ordunisuc2  7548  limsssuc  7554  wfrlem10  7953  tz7.48lem  8066  sdomdif  8653  pssinf  8716  unblem1  8758  supnub  8914  infnlb  8944  elirrv  9048  inf3lem6  9084  cantnflem1  9140  cardne  9382  cardsdomel  9391  carddom2  9394  cardmin2  9415  alephnbtwn  9485  infdif2  9620  fin4en1  9719  fin23lem31  9753  isf32lem5  9767  isf34lem4  9787  cfpwsdom  9994  fpwwe2  10053  addnidpi  10311  genpnnp  10415  btwnnz  12046  prime  12051  qsqueeze  12582  xralrple  12586  xmullem2  12646  xmulneg1  12650  ssfzoulel  13119  elfznelfzob  13131  bcval4  13655  seqcoll  13810  hashtpg  13831  swrd0  14008  fsumcvg  15057  fsumsplit  15085  fprodcvg  15272  fprodsplit  15308  dvdsle  15648  divalglem8  15739  bitsinv1lem  15778  2mulprm  16025  pockthg  16230  prmunb  16238  vdwlem6  16310  ramlb  16343  gsumzsplit  18976  opsrtoslem2  20193  obselocv  20800  elcls  21609  fbasrn  22420  ufilb  22442  ufilmax  22443  rnelfmlem  22488  alexsubALTlem4  22586  tsmssplit  22687  recld2  23349  logbgcd1irr  25299  fsumharmonic  25516  chtub  25715  lgsne0  25838  axlowdim  26674  wlkp1lem5  27386  wlkp1lem6  27387  cyclnspth  27508  eupth2lem3lem4  27937  cvnsym  29994  cvntr  29996  atcvati  30090  rmounid  30186  ballotlemfc0  31649  ballotlemfcc  31650  ballotlemfrcn0  31686  ballotlemirc  31688  acycgr2v  32294  cusgracyclt3v  32300  fmlasucdisj  32543  dfpo2  32888  sltres  33066  nosupbnd2lem1  33112  nocvxminlem  33144  nn0prpw  33568  onsucconni  33682  onint1  33694  icorempo  34514  relowlpssretop  34527  fvineqsneq  34575  lindsenlbs  34768  poimirlem16  34789  poimirlem26  34799  fdc  34901  lsatcvat  36066  hlrelat2  36419  ltltncvr  36439  islln2a  36533  islpln2a  36564  islvol2aN  36608  rencldnfilem  39295  ss2iundf  39882  uneqsn  40251  radcnvrat  40523  stoweidlem34  42196  oddneven  43686
  Copyright terms: Public domain W3C validator