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

Step	Hyp	Ref	Expression
1		notnotr 132	. . 3 ⊢ (¬ ¬ 𝜓 → 𝜓)
2		con3d.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	1, 2	syl5 34	. 2 ⊢ (𝜑 → (¬ ¬ 𝜓 → 𝜒))
4	3	con1d 147	1 ⊢ (𝜑 → (¬ 𝜒 → ¬ 𝜓))

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  912  aleximi  1839  nelcon3d  3048  rexim  3153  spcimegf  3495  spcimedv  3500  rspcimedv  3518  ssneld  3889  sscon  4039  difrab  4209  disjord  5027  disjiund  5029  dtru  5248  otiunsndisj  5388  wereu2  5533  frpomin  6172  ndmfv  6725  dff3  6897  soisores  7114  releldmdifi  7794  funeldmdif  7797  ressuppssdif  7905  wfrlem10  8042  tz7.49  8159  oaord  8253  oalimcl  8266  omord2  8273  omcan  8275  omeulem1  8288  oeord  8294  oecan  8295  nnaord  8325  nnmord  8338  nneob  8359  omsmo  8361  domtriord  8770  pssnn  8824  isinf  8867  pssnnOLD  8872  frfi  8894  fisupg  8897  difinf  8919  supmo  9046  infmo  9089  alephord  9654  fin17  9973  isfin7-2  9975  fin1a2lem12  9990  fpwwe2lem12  10221  prub  10573  genpnnp  10584  ltaddpr  10613  prlem936  10626  ltadd2  10901  ltord1  11323  ltmul1  11647  lt2msq  11682  nnge1  11823  nzadd  12190  zeo  12228  irradd  12534  irrmul  12535  mul2lt0bi  12657  supxrun  12871  supxrgtmnf  12884  ssfzoulel  13301  zesq  13758  bccmpl  13840  fundmge2nop0  14023  repswswrd  14314  s3iunsndisj  14496  lcmftp  16156  prm2orodd  16211  coprm  16231  prmndvdsfaclt  16245  hashgcdeq  16305  prmreclem3  16434  vdwnnlem2  16512  latnlej2  17919  mgm2nsgrplem3  18301  f1omvdco2  18794  oddvds  18893  gexdvds  18927  frgpnabl  19214  ablfac1eulem  19413  ablfac1eu  19414  psgnodpm  20504  obselocv  20644  1marepvmarrepid  21426  mdetunilem9  21471  t1connperf  22287  txindislem  22484  fbasrn  22735  isufil2  22759  ufileu  22770  filufint  22771  ufilen  22781  fin1aufil  22783  alexsubALTlem4  22901  ptcmplem2  22904  itg2gt0  24612  cosord  25374  argimgt0  25454  logdivlt  25463  logrec  25600  dcubic  25683  wilthlem2  25905  bposlem3  26121  dchrisum0fno1  26346  numedglnl  27189  nbumgr  27389  uhgrnbgr0nb  27396  cusgrfi  27500  vtxduhgr0nedg  27534  uhgrvd00  27576  wlkp1lem6  27720  2wspmdisj  28374  chnlen0  29479  staddi  30281  stadd3i  30283  strlem1  30285  atoml2i  30418  prmdvdsbc  30804  psgnfzto1stlem  31040  madjusmdetlem1  31445  madjusmdetlem2  31446  hasheuni  31719  sitgaddlemb  31981  eulerpartlemb  32001  ballotlemfc0  32125  ballotlemfcc  32126  acycgrislfgr  32781  umgracycusgr  32783  acycgrsubgr  32787  funeldmb  33407  dfon2lem6  33434  exnel  33448  sltres  33551  nosepssdm  33575  nosupbnd1lem1  33597  sletr  33647  nn0prpwlem  34197  waj-ax  34289  bj-dtru  34685  sucneqond  35222  wl-spae  35366  wl-ax11-lem3  35424  lindsadd  35456  matunitlindflem1  35459  poimirlem26  35489  poimirlem28  35491  poimirlem31  35494  areacirc  35556  pridlc3  35917  lkreqN  36870  atlrelat1  37021  2llnneN  37109  cdlemg4c  38312  mapdh8e  39484  sticksstones1  39771  sn-dtru  39851  mulgt0con1dlem  40076  nna4b4nsq  40141  vk15.4j  41762  isosctrlem1ALT  42168  afvres  44279  otiunsndisjX  44386  fmtnoinf  44604  requad2  44691  copisnmnd  44979  dig1  45570  rrxsphere  45710