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

Theorem con3d 149
Description: A contraposition deduction. Deduction form of con3 150. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
con3d.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
con3d (𝜑 → (¬ 𝜒 → ¬ 𝜓))

Proof of Theorem con3d
StepHypRef Expression
1 notnotr 128 . . 3 (¬ ¬ 𝜓𝜓)
2 con3d.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl5 34 . 2 (𝜑 → (¬ ¬ 𝜓𝜒))
43con1d 141 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:  con3  150  con3rr3  152  nsyld  155  nsyli  156  mth8  159  pm2.52  168  pm5.21ndd  368  bija  369  con3dimp  395  orim12dALT  895  aleximi  1907  nelcon3d  3058  rexim  3156  spcimegf  3438  spcimedv  3443  rspcimedv  3462  ssneld  3754  sscon  3895  difrab  4049  disjord  4775  disjiund  4777  dtru  4988  otiunsndisj  5113  wereu2  5246  ndmfv  6359  dff3  6515  soisores  6720  ressuppssdif  7467  wfrlem10  7577  tz7.49  7693  oaord  7781  oalimcl  7794  omord2  7801  omcan  7803  omeulem1  7816  oeord  7822  oecan  7823  nnaord  7853  nnmord  7866  nneob  7886  omsmo  7888  domtriord  8262  isinf  8329  pssnn  8334  frfi  8361  fisupg  8364  difinf  8386  supmo  8514  infmo  8557  fiinfg  8561  alephord  9098  fin17  9418  isfin7-2  9420  fin1a2lem12  9435  fpwwe2lem13  9666  prub  10018  genpnnp  10029  ltaddpr  10058  prlem936  10071  ltadd2  10343  ltord1  10756  prodge0OLD  11072  ltmul1  11075  lt2msq  11110  nnge1  11248  nzadd  11627  zeo  11665  irradd  12015  irrmul  12016  mul2lt0bi  12139  supxrun  12351  supxrgtmnf  12364  ssfzoulel  12770  zesq  13194  bccmpl  13300  fundmge2nop0  13476  repswswrd  13740  s3iunsndisj  13917  lcmftp  15557  prm2orodd  15611  coprm  15630  prmndvdsfaclt  15642  hashgcdeq  15701  prmreclem3  15829  vdwnnlem2  15907  latnlej2  17279  mgm2nsgrplem3  17615  f1omvdco2  18075  oddvds  18173  gexdvds  18206  frgpnabl  18485  ablfac1eulem  18679  ablfac1eu  18680  psgnodpm  20149  obselocv  20289  1marepvmarrepid  20599  mdetunilem9  20644  t1connperf  21460  txindislem  21657  fbasrn  21908  isufil2  21932  ufileu  21943  filufint  21944  ufilen  21954  fin1aufil  21956  alexsubALTlem4  22074  ptcmplem2  22077  itg2gt0  23747  cosord  24499  argimgt0  24579  logdivlt  24588  logrec  24722  dcubic  24794  wilthlem2  25016  bposlem3  25232  dchrisum0fno1  25421  numedglnl  26261  nbumgr  26466  uhgrnbgr0nb  26473  cusgrfi  26589  vtxduhgr0nedg  26623  uhgrvd00  26665  wlkp1lem6  26810  2wspmdisj  27519  chnlen0  28643  staddi  29445  stadd3i  29447  strlem1  29449  atoml2i  29582  psgnfzto1stlem  30190  madjusmdetlem1  30233  madjusmdetlem2  30234  hasheuni  30487  sitgaddlemb  30750  eulerpartlemb  30770  ballotlemfc0  30894  ballotlemfcc  30895  funeldmb  31999  dfon2lem6  32029  exnel  32044  frpomin  32075  sltres  32152  nosepssdm  32173  nosupbnd1lem1  32191  sletr  32220  nn0prpwlem  32654  waj-ax  32750  bj-dtru  33133  sucneqond  33550  wl-spae  33643  wl-ax11-lem3  33698  matunitlindflem1  33738  poimirlem26  33768  poimirlem28  33770  poimirlem31  33773  areacirc  33837  pridlc3  34204  lkreqN  34979  atlrelat1  35130  2llnneN  35217  cdlemg4c  36421  mapdh8e  37594  vk15.4j  39259  isosctrlem1ALT  39692  afvres  41772  otiunsndisjX  41821  fmtnoinf  41976  copisnmnd  42337  dig1  42930
  Copyright terms: Public domain W3C validator