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

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

Proof of Theorem con3d
StepHypRef Expression
1 notnotr 132 . . 3 (¬ ¬ 𝜓𝜓)
2 con3d.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2syl5 34 . 2 (𝜑 → (¬ ¬ 𝜓𝜒))
43con1d 147 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  156  con3rr3  158  nsyld  159  nsyli  160  mth8  163  pm5.21ndd  381  bija  382  con3dimp  409  orim12dALT  905  aleximi  1823  nelcon3d  3132  rexim  3238  spcimegf  3586  spcimedv  3591  rspcimedv  3611  ssneld  3966  sscon  4112  difrab  4274  disjord  5045  disjiund  5047  dtru  5262  otiunsndisj  5401  wereu2  5545  ndmfv  6693  dff3  6858  soisores  7069  releldmdifi  7733  funeldmdif  7736  ressuppssdif  7840  wfrlem10  7953  tz7.49  8070  oaord  8162  oalimcl  8175  omord2  8182  omcan  8184  omeulem1  8197  oeord  8203  oecan  8204  nnaord  8234  nnmord  8247  nneob  8268  omsmo  8270  domtriord  8651  isinf  8719  pssnn  8724  frfi  8751  fisupg  8754  difinf  8776  supmo  8904  infmo  8947  alephord  9489  fin17  9804  isfin7-2  9806  fin1a2lem12  9821  fpwwe2lem13  10052  prub  10404  genpnnp  10415  ltaddpr  10444  prlem936  10457  ltadd2  10732  ltord1  11154  ltmul1  11478  lt2msq  11513  nnge1  11653  nzadd  12018  zeo  12056  irradd  12360  irrmul  12361  mul2lt0bi  12483  supxrun  12697  supxrgtmnf  12710  ssfzoulel  13119  zesq  13575  bccmpl  13657  fundmge2nop0  13838  repswswrd  14134  s3iunsndisj  14316  lcmftp  15968  prm2orodd  16023  coprm  16043  prmndvdsfaclt  16055  hashgcdeq  16114  prmreclem3  16242  vdwnnlem2  16320  latnlej2  17669  mgm2nsgrplem3  18023  f1omvdco2  18505  oddvds  18604  gexdvds  18638  frgpnabl  18924  ablfac1eulem  19123  ablfac1eu  19124  psgnodpm  20660  obselocv  20800  1marepvmarrepid  21112  mdetunilem9  21157  t1connperf  21972  txindislem  22169  fbasrn  22420  isufil2  22444  ufileu  22455  filufint  22456  ufilen  22466  fin1aufil  22468  alexsubALTlem4  22586  ptcmplem2  22589  itg2gt0  24288  cosord  25043  argimgt0  25122  logdivlt  25131  logrec  25268  dcubic  25351  wilthlem2  25573  bposlem3  25789  dchrisum0fno1  26014  numedglnl  26856  nbumgr  27056  uhgrnbgr0nb  27063  cusgrfi  27167  vtxduhgr0nedg  27201  uhgrvd00  27243  wlkp1lem6  27387  2wspmdisj  28043  chnlen0  29148  staddi  29950  stadd3i  29952  strlem1  29954  atoml2i  30087  prmdvdsbc  30458  psgnfzto1stlem  30669  madjusmdetlem1  30991  madjusmdetlem2  30992  hasheuni  31243  sitgaddlemb  31505  eulerpartlemb  31525  ballotlemfc0  31649  ballotlemfcc  31650  acycgrislfgr  32296  umgracycusgr  32298  acycgrsubgr  32302  funeldmb  32903  dfon2lem6  32930  exnel  32944  frpomin  32975  sltres  33066  nosepssdm  33087  nosupbnd1lem1  33105  sletr  33134  nn0prpwlem  33567  waj-ax  33659  bj-dtru  34036  sucneqond  34528  wl-spae  34643  wl-ax11-lem3  34700  lindsadd  34766  matunitlindflem1  34769  poimirlem26  34799  poimirlem28  34801  poimirlem31  34804  areacirc  34868  pridlc3  35232  lkreqN  36186  atlrelat1  36337  2llnneN  36425  cdlemg4c  37628  mapdh8e  38800  sn-dtru  38989  vk15.4j  40739  isosctrlem1ALT  41145  afvres  43248  otiunsndisjX  43355  fmtnoinf  43575  requad2  43665  copisnmnd  43953  dig1  44596  rrxsphere  44663
  Copyright terms: Public domain W3C validator