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

Theorem con2d 121
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 118 . . 3 (¬ ¬ 𝜓𝜓)
2 con2d.1 . . 3 (𝜑 → (𝜓 → ¬ 𝜒))
31, 2syl5 33 . 2 (𝜑 → (¬ ¬ 𝜓 → ¬ 𝜒))
43con4d 110 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  122  mt2d  123  pm3.2im  152  exists2  2445  necon2bd  2693  spcimegf  3149  spcegf  3151  spcimedv  3154  rspcimedv  3173  minel  3860  disjxun  4432  sotric  4827  sotrieq  4828  poirr2  5274  funun  5675  imadif  5713  soisoi  6292  onnminsb  6708  oneqmin  6709  ordunisuc2  6748  limsssuc  6754  wfrlem10  7122  tz7.48lem  7235  sdomdif  7804  pssinf  7866  unblem1  7908  supnub  8061  infnlb  8091  elirrv  8197  inf3lem6  8223  cantnflem1  8279  cardne  8484  cardsdomel  8493  carddom2  8496  cardmin2  8517  alephnbtwn  8587  infdif2  8725  fin4en1  8824  fin23lem31  8858  isf32lem5  8872  isf34lem4  8892  cfpwsdom  9094  fpwwe2  9153  addnidpi  9411  genpnnp  9515  btwnnz  11102  prime  11106  qsqueeze  11587  xralrple  11591  xmullem2  11646  xmulneg1  11650  ssfzoulel  12109  elfznelfzob  12121  bcval4  12606  seqcoll  12750  hashtpg  12764  swrd0  12924  fsumcvg  13938  fsumsplit  13966  fprodcvg  14144  fprodsplit  14180  dvdsle  14510  divalglem8  14542  bitsinv1lem  14577  pockthg  15012  prmunb  15020  vdwlem6  15098  ramlb  15139  gsumzsplit  17721  opsrtoslem2  18867  obselocv  19449  elcls  20246  fbasrn  21057  ufilb  21079  ufilmax  21080  rnelfmlem  21125  alexsubALTlem4  21223  tsmssplit  21324  recld2  21990  fsumharmonic  24098  chtub  24301  lgsne0  24422  axlowdim  25152  nbusgra  25317  nbgranself  25323  usgrasscusgra  25372  cyclnspth  25520  eupath2lem3  25867  cvnsym  28106  cvntr  28108  atcvati  28202  ballotlemfc0  29479  ballotlemfcc  29480  ballotlemfrcn0  29516  ballotlemirc  29518  ballotlemfrcn0OLD  29554  ballotlemircOLD  29556  dfpo2  30546  sltres  30702  nodenselem5  30725  nocvxminlem  30730  nobndup  30740  nobnddown  30741  nofulllem5  30746  nn0prpw  31128  onsucconi  31246  onint1  31258  icorempt2  31975  relowlpssretop  31988  lindsenlbs  32173  poimirlem16  32194  poimirlem26  32204  fdc  32311  lsatcvat  32856  hlrelat2  33208  ltltncvr  33228  islln2a  33322  islpln2a  33353  islvol2aN  33397  rencldnfilem  35903  ss2iundf  36490  radcnvrat  37020  stoweidlem34  38331  oddneven  39294  nbgrssovtx  39986  1wlkp1lem5  40286  1wlkp1lem6  40287  cyclnsPth  40406  eupth2lem3lem4  40799
  Copyright terms: Public domain W3C validator