Theorem 3imtr4i 329

Description: A mixed syllogism inference, useful for applying a definition to both sides of an implication.

Hypotheses

Ref	Expression
3imtr4.1	|- (ph -> ps)
3imtr4.2	|- (ch <-> ph)
3imtr4.3	|- (th <-> ps)

Assertion

Ref	Expression
3imtr4i	|- (ch -> th)

Proof of Theorem 3imtr4i

Step	Hyp	Ref	Expression
1		3imtr4.2	. . 3 |- (ch <-> ph)
2		3imtr4.1	. . 3 |- (ph -> ps)
3	1, 2	sylbi 237	. 2 |- (ch -> ps)
4		3imtr4.3	. 2 |- (th <-> ps)
5	3, 4	sylibr 264	1 |- (ch -> th)

Syntax hints:   -> wi 3   <-> wb 231

This theorem is referenced by:  orbidiOLD 1084  hbex 1671  hbor 1673  hban 1674  hbbi 1675  hb3or 1676  hb3an 1677  hbe1 1681  19.29r 1738  19.30 1751  sbimi 1846  hbs1f 1862  hbeu1 2076  hbeu 2077  sb8eu 2079  hbmo1 2096  hbmo 2097  euan 2118  2exeu 2138  2eu6 2146  hbab1 2160  hbab 2161  hbxfr 2271  hbeq 2274  hbel 2275  hbne 2383  hbnel 2384  hbral 2426  hbra1 2428  hbra2 2429  hbrex 2430  hbre1 2431  ralimi2 2445  reximi2 2477  r19.28av 2504  r19.29r 2506  r19.30 2507  ralcom2 2521  hbreu 2527  hbreu1 2529  elisset 2578  reurex 2717  sbcel12g 2817  sbceqg 2818  hbss 2877  sseq2 2898  rabss2 2947  hbdif 2980  hbun 3007  hbin 3044  undif4 3165  r19.2zb 3191  ralf0 3207  hbpw 3267  hbpr 3301  difprsn 3353  snsspw 3369  hbuni 3404  hbeqel 3416  uniin 3418  reucl 3431  hbint 3442  intss 3453  iuniin 3476  iuneq1 3479  iuneq2 3482  iunpwss 3538  hbbr 3586  eunex 3696  exss 3711  opprc3 3738  pwunss 3770  poeq2 3787  soeq2 3800  freq2 3820  trssord 3860  hbsuc 3913  reusv2lem2 4000  onminex 4063  nlimsucg 4095  xpss 4221  hbrel 4238  coeq1 4282  coeq2 4283  cnveq 4295  hbcnv 4299  dmeq 4315  dmin 4322  hbrn 4351  dmcoss 4365  rncoeq 4369  resiexg 4406  dminss 4477  imainss 4478  dfco2a 4534  funeq 4582  hbfun 4585  fununi 4620  hbfn 4647  2elresin 4661  zfrep6 4679  hbf 4696  fco 4707  hbf1 4734  f1co 4739  hbfo 4743  fof 4744  foco 4755  hbf1o 4760  f1ocnv 4774  f1ores 4776  f1oco 4783  fopab2 4927  hbiso 5002  isocnv 5006  isotr 5009  isotrALT 5010  oprabid 5041  difxp 5191  hbiota1 5261  sb8iota 5266  iotaex 5273  reiota4 5281  smores 5303  tz7.48lem 5368  tz7.49 5375  eqer 5529  map0 5607  ixpeq2 5618  enssdom 5646  fiprc 5698  sbthlem9 5727  mapunen 5831  infensuc 5837  zfreg 5975  zfreg2 5976  dfom3 6016  infensucOLD 6025  scott0 6151  r0weon 6211  elomsubsd 6241  fodomnumlem 6273  domtriomlemOLDOLD 6369  dominf 6371  axdc4lem 6381  axcclem 6383  ac9 6399  ac6n 6401  ac9s 6410  dominfac 6522  cdainfOLD 6531  ltsopq 6670  1pr 6712  reclem2pr 6752  ltsosr 6798  ltsor 6856  ssxr 7001  ltadd2i 7051  recgt0ii 7425  ltmul1ii 7432  peano2nn 7553  sup2 7708  peano2uz2 7868  zq 7898  irradd 7915  irrmul 7916  elioc2 8016  elico2 8017  elicc2 8018  eluzp1p1 8063  peano2uz 8077  sumsqne0i 8379  nnesqi 8412  recvalzi 8639  cjdivi 8640  cau5ii 8670  fsumser0fi 8773  fsumser1fi 8774  ser0cji 8837  climcmplem 8909  efltbi 9188  reeff1o 9207  sin02gt0 9260  infxpidmlem10OLD 9360  clatl 9826  fctop 9921  cctop 9923  retopbas 9932  blssioo 10207  metcnp4 10265  ablmul 10460  sspval 10742  nmobndseqi 10802  cosh111lem2 11096  efifolem4 11106  efifo 11110  efif1lem1 11111  efif1lem2 11112  symgf 11194  symggrpi 11195  fine 11203  abfi 11208  fgfil 11286  tosdir 11354  axhcompl 11496  hhcmpl 11696  chsscmi 11737  chcmhi 11738  shscli 11906  shunssi 11962  shsleji 11963  shlubi 11971  pjoml3i 12152  cmcmlem 12157  nonbooli 12221  5oalem2 12225  3oalem2 12233  lnopco0i 12556  bra11 12668  pjnmopi 12708  pjnormssi 12729  pj3lem1 12768  mdsldmd1i 12892  hatomistici 12923  cvexchi 12930  cmdmdi 12978  mddmdin0i 12992  cdj3lem3b 13001  bnj48 13370  bnj142 13412  bnj180 13432  bnj572 13475  bnj899 13745  bnj945 13773  bnj1208 13911  bnj98 14150  bnj545 14200  bnj556 14209  bnj557 14210  bnj583 14225  bnj607 14233  bnj944 14269  bnj949 14270  bnj999 14294  bnj1067 14328  r19.30OLD 14694  fundmpss 14714  fresin 14717  setinds 14725  elpotr 14728  dfon2lem8 14737  omopthlem1 14748  trpredlem1 14826  trpredrec 14837  poseq 14854  wfrlem5 14861  wfrlem9 14865  frrlem5 14885  sltval2 14909  noreson 14913  axsltsolem1 14921  axfelem15 14960  txpss3v 14997  limitssson 15019  meran1 15182  arg-ax 15187  nxtor 15281  evpexun 15291  neiopne 15325  hbcp 15500  npincppr 15501  dstr 15516  tolat 15631  latdir 15643  ablcomgrp 15698  fprodsub 15738  trinv 15754  eqindhome 15913  cntrsetlem 16052  issubcat 16248  taralt 16282  elomsubsdOLD 16479  alexsublem4 16525  reconnlem3 16533  reconnlem4 16534  reconnlem5 16535  neibastop2lem4 16607  fnejoin2 16616  filssufil 16656  difxpOLD 16775  hbixp1 16810  firnfi3 16828  sdc 16896  fdc 16897  fsumltisumi 16908  caushft 16936  iirev 16956  iihalf1 16957  iihalf2 16958  iimulcl 16959  sstotbnd 17021  bndss 17027  heiborlem15 17054  heiborlem16 17055  heiborlem30 17069  heiborlem35 17074  fldcrng 17237  flddmn 17291  ax10ext 17449  iotaexeu 17467  smoresOLD 17529

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 232

Copyright terms: Public domain