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  jcn  165  pm5.21ndd  384  bija  385  con3dimp  412  orim12dALT  909  aleximi  1833  nelcon3d  3106  rexim  3207  spcimegf  3540  spcimedv  3545  rspcimedv  3565  ssneld  3920  sscon  4069  difrab  4232  disjord  5021  disjiund  5023  dtru  5239  otiunsndisj  5378  wereu2  5520  ndmfv  6679  dff3  6847  soisores  7063  releldmdifi  7730  funeldmdif  7733  ressuppssdif  7838  wfrlem10  7951  tz7.49  8068  oaord  8160  oalimcl  8173  omord2  8180  omcan  8182  omeulem1  8195  oeord  8201  oecan  8202  nnaord  8232  nnmord  8245  nneob  8266  omsmo  8268  domtriord  8651  isinf  8719  pssnn  8724  frfi  8751  fisupg  8754  difinf  8776  supmo  8904  infmo  8947  alephord  9490  fin17  9809  isfin7-2  9811  fin1a2lem12  9826  fpwwe2lem13  10057  prub  10409  genpnnp  10420  ltaddpr  10449  prlem936  10462  ltadd2  10737  ltord1  11159  ltmul1  11483  lt2msq  11518  nnge1  11657  nzadd  12022  zeo  12060  irradd  12364  irrmul  12365  mul2lt0bi  12487  supxrun  12701  supxrgtmnf  12714  ssfzoulel  13130  zesq  13587  bccmpl  13669  fundmge2nop0  13850  repswswrd  14141  s3iunsndisj  14323  lcmftp  15973  prm2orodd  16028  coprm  16048  prmndvdsfaclt  16060  hashgcdeq  16119  prmreclem3  16247  vdwnnlem2  16325  latnlej2  17676  mgm2nsgrplem3  18080  f1omvdco2  18571  oddvds  18670  gexdvds  18704  frgpnabl  18991  ablfac1eulem  19190  ablfac1eu  19191  psgnodpm  20280  obselocv  20420  1marepvmarrepid  21183  mdetunilem9  21228  t1connperf  22044  txindislem  22241  fbasrn  22492  isufil2  22516  ufileu  22527  filufint  22528  ufilen  22538  fin1aufil  22540  alexsubALTlem4  22658  ptcmplem2  22661  itg2gt0  24367  cosord  25126  argimgt0  25206  logdivlt  25215  logrec  25352  dcubic  25435  wilthlem2  25657  bposlem3  25873  dchrisum0fno1  26098  numedglnl  26940  nbumgr  27140  uhgrnbgr0nb  27147  cusgrfi  27251  vtxduhgr0nedg  27285  uhgrvd00  27327  wlkp1lem6  27471  2wspmdisj  28125  chnlen0  29230  staddi  30032  stadd3i  30034  strlem1  30036  atoml2i  30169  prmdvdsbc  30561  psgnfzto1stlem  30795  madjusmdetlem1  31180  madjusmdetlem2  31181  hasheuni  31452  sitgaddlemb  31714  eulerpartlemb  31734  ballotlemfc0  31858  ballotlemfcc  31859  acycgrislfgr  32507  umgracycusgr  32509  acycgrsubgr  32513  funeldmb  33114  dfon2lem6  33141  exnel  33155  frpomin  33186  sltres  33277  nosepssdm  33298  nosupbnd1lem1  33316  sletr  33345  nn0prpwlem  33778  waj-ax  33870  bj-dtru  34249  sucneqond  34777  wl-spae  34919  wl-ax11-lem3  34977  lindsadd  35043  matunitlindflem1  35046  poimirlem26  35076  poimirlem28  35078  poimirlem31  35081  areacirc  35143  pridlc3  35504  lkreqN  36459  atlrelat1  36610  2llnneN  36698  cdlemg4c  37901  mapdh8e  39073  sn-dtru  39390  mulgt0con1dlem  39569  vk15.4j  41221  isosctrlem1ALT  41627  afvres  43715  otiunsndisjX  43822  fmtnoinf  44040  requad2  44128  copisnmnd  44416  dig1  45009  rrxsphere  45149
  Copyright terms: Public domain W3C validator